4.2. Outline of the proof
For the proof of the first implication, I have followed the classical strategy based on constructing a family of open sets indexed by rationals. Although there are variants that use particular subsets such as the dyadic rationals, here we have opted for a construction over \mathbb{Q} \cap [0,1], following usual versions of the lemma found in the literature. Even so, the outline presented below is also the result of the proof process in Lean, which took shape as the various obstacles that came up were resolved.
Suppose that X is a normal space, and let C_1 and C_2 be two non-empty disjoint closed sets of X.
Consider the open set U_1 = X. Consider the closed set C_1 and the open set C_2^c and apply the characterisation of normal spaces (3.14), obtaining another open set U_0 such that
C_1 \subseteq U_0 \subseteq \overline{U_0} \subseteq C_2^c \subseteq U_1 = X
We can do the same for the closed set \overline{U_0} and the open set C_2^c, obtaining, for example, U_{\frac{1}{2}} such that
C_1 \subseteq U_0 \subseteq \overline{U_0} \subseteq U_{\frac{1}{2}} \subseteq \overline{U_{\frac{1}{2}}} \subseteq C_2^c \subseteq U_1
Iterating this process, we are going to construct a sequence of open sets over \mathbb{Q}\cap[0, 1], \{U_p | p \in \mathbb{Q}\cap[0, 1]\}, such that
The property (★)
\forall p , q \in \mathbb{Q}, p < q \implies \overline{U_p} \subseteq U_q
Once we have this sequence, we will extend it to all of \mathbb{Q}, obtaining what in Lean will be a function G : \mathbb{Q} \to \mathcal{P}(X). Afterwards, we will define another function F on X that assigns to each x \in X the set
F(x) = \{p \in \mathbb{Q} ~|~ x \in G(p)\}
Finally, we will take the function f : X \to [0, 1] defined by
f(x) = \textnormal{inf}~F(x)
This will be the function we use. We will have to prove that it indeed takes values in [0, 1], that it is continuous and that it separates our closed sets.
However, once these functions are constructed, this last step is relatively easy. The main difficulty in formalising this proof has been constructing the function G and proving its properties.
As can be seen in the first iterations of the construction of each U_q, this sequence is built by induction. In order to do induction over the rationals, we rely on the fact that they are countable, and, in particular, on the fact that \mathbb{Q}\cap[0, 1] is. We are going to find a bijective (invertible) function f : \mathbb{N} \to \mathbb{Q} \cap [0, 1], such that f(0) = 1 and f(1) = 0. This will serve us to construct each U_q.
Then, to prove that condition (★) indeed holds, we will need to use induction on two variables. To do so, we will use that the lexicographic order on (\mathbb{N} \times \mathbb{N}), defined by (n, m) < (n', m') \iff n<n' \lor (n=n' \land m<m'), is a well-founded relation, and therefore admits induction on pairs of naturals.
The main difficulty of this construction has been finding the right objects to formalise the ideas of the proof, such as the countability of the rationals or the lexicographic order, and learning the correct way to work with certain structures in Lean, such as defining recursive functions with an unusual recursion.