Urysohn's lemma

In topology, Urysohn's lemma is a lemma that states that a topological space is normal if and only if any two disjoint closed subsets can be separated by a continuous function.

[1] Urysohn's lemma is commonly used to construct continuous functions with various properties on normal spaces.

It is widely applicable since all metric spaces and all compact Hausdorff spaces are normal.

The lemma is generalised by (and usually used in the proof of) the Tietze extension theorem.

The lemma is named after the mathematician Pavel Samuilovich Urysohn.

are said to be separated by a continuous function if there exists a continuous function

are separated by a function then so are their closures.

A normal space is a topological space in which any two disjoint closed sets can be separated by neighbourhoods.

Urysohn's lemma states that a topological space is normal if and only if any two disjoint closed sets can be separated by a continuous function.

in which every two disjoint closed subsets

are precisely separated by a continuous function is perfectly normal.

Urysohn's lemma has led to the formulation of other topological properties such as the 'Tychonoff property' and 'completely Hausdorff spaces'.

For example, a corollary of the lemma is that normal T1 spaces are Tychonoff.

is normal if and only if, for any two non-empty closed disjoint subsets

there exists a continuous map

The proof proceeds by repeatedly applying the following alternate characterization of normality.

is closed, then there exists an open

be disjoint closed subsets of

The main idea of the proof is to repeatedly apply this characterization of normality to

, continuing with the new sets built on every step.

The sets we build are indexed by dyadic fractions.

, we construct an open subset

expand outwards in layers from

: This construction proceeds by mathematical induction.

For the base step, we define two extra sets

Note that this is vacuously satisfied for

, we can find an open set and a closed set such that The above three conditions are then verified.

Using the fact that the dyadic rationals are dense, it is then not too hard to show that

sets in order to work.

The Mizar project has completely formalised and automatically checked a proof of Urysohn's lemma in the URYSOHN3 file.