Formalising Mathematics with Lean

4. Urysohn's Lemma🔗

Urysohn's lemma is one of the central results of general topology. Its importance lies in the fact that it makes it possible to characterise the normality of a topological space in terms of continuous functions.

While the classical separation axioms require the existence of disjoint open sets to separate points or sets, there are versions that require separation by continuous functions. These versions are more restrictive and, therefore, define stronger properties. However, Urysohn's lemma shows that in the case of normal spaces this does not happen: separating closed sets by continuous functions is equivalent to doing so by open sets.

This result has key applications, such as its use in the proof of Urysohn's metrisation theorem, which provides sufficient conditions for a space to be metrisable. Moreover, the proof of the lemma is of great interest in itself, especially for our purposes, since it is based on an explicit and non-trivial construction of the desired function. It is precisely the construction of this function that a good part of this section will be devoted to.

  1. Theorem 4.1 (Urysohn's Lemma)
  2. 4.1. The converse
  3. 4.2. Outline of the proof
  4. 4.3. Construction of the sequence of open sets
  5. 4.4. Construction of a separating continuous function
  6. 4.5. The proof
  7. 4.6. The Mathlib proof