4.6. The Mathlib proof🔗

The proof of Urysohn's lemma that I have described in this chapter was implemented by me completely independently of the Mathlib one, which I did not read until I had completely written my proof. To close this chapter I would like to make a brief comparison of the two.

The implementation found in Mathlib is documented (Lean Prover Community, 2023)Lean Prover Community, 2023. “Urysohn's lemma”. Last accessed: June 22, 2025..

As we mentioned at the beginning of the chapter, the most complicated part of the proof has been constructing the function G, since it requires complete induction to construct the open sets and induction on two variables to prove their properties. Indeed, in the Mathlib documentation, they write:

Most sources prove Urysohn's lemma using a family of open sets indexed by the dyadic rational numbers in [0, 1]. There are many technical difficulties when formalising this proof (e.g., one needs to formalise the "dyadic induction", and then prove that the resulting family of open sets is monotone).

Indeed, it is possible to build the sequence we have constructed taking only the dyadics, but one runs into problems similar to the ones we have encountered. The goal of the Mathlib proof is, therefore, to avoid this complication. Below we will see an outline of the Mathlib proof.

Let X be a normal space. Let \mathcal{CU}_X be the set of normal pairs of X, that is, the pairs of the form (C, U) with U open, C closed and C \subseteq U. We define the functions:

\begin{array}{ccrclcccrcl} L & : & \mathcal{CU}_X & \longrightarrow & \mathcal{CU}_X & ~~\textnormal{and}~~ & R & : & \mathcal{CU}_X & \longrightarrow & \mathcal{CU}_X \\ & & (C, U) & \longmapsto & (C, V) & & & & (C, V) & \longmapsto & (\overline{V}, U) \end{array}

Where V is the result of applying the characterisation of normal spaces (3.14) to the corresponding pair (C, U).

Moreover, for each (C, U) \in \mathcal{CU}_X consider the sequence of functions \{f_n^{(C, U)} : X \to \mathbb{R}\}_{n\in \mathbb{N}} given by

\left\{ \begin{array}{lclc} f_0^{(C, U)}(x) & = & \chi_{U^c}(x) & \\ & & & \\ f_{n+1}^{(C, U)}(x) & = & \dfrac{f_n^{L(C, U)}(x) + f_n^{R(C, U)}(x)}{2}, & n = 0, 1, \dots \end{array} \right.

It can be proved that this is a monotone sequence of functions such that, for each pair (C, U) and each n \in \mathbb{N}, f_n^{(C, U)}(x) =0, \forall x \in C, f_n^{(C, U)}(x) = 1,\forall x \in D, and f_n^{(C, U)}(x) \in [0, 1],\forall x \in X.

In particular, let C and D be the disjoint closed sets we want to separate and consider the pair (C, D^c) \in \mathcal{CU}_X. Let f : X \to \mathbb{R} be the function given by

f(x) = \lim_{n \to \infty} f_n^{(C, D^c)}

Then f is a continuous function that separates C and D.