Editing Urysohn's lemma (section)

==Proof sketch==
[[File:Urysohn-function01.svg|thumb|260x260px|Illustration of the first few sets built as part of the proof.]]
The proof proceeds by repeatedly applying the following alternate characterization of normality. If <math>X</math> is a normal space, <math>Z</math> is an [[Open set|open]] subset of <math>X</math>, and <math>Y\subseteq Z</math> is closed, then there exists an open <math>U</math> and a closed <math>V</math> such that <math>Y\subseteq U\subseteq V\subseteq Z</math>. 

Let <math>A</math> and <math>B</math> be disjoint closed subsets of <math>X</math>. The main idea of the proof is to repeatedly apply this characterization of normality to <math>A</math> and <math>B^\complement</math>, continuing with the new sets built on every step. 

The sets we build are indexed by [[Dyadic rational|dyadic fractions]]. For every dyadic fraction <math>r \in (0, 1)</math>, we construct an open subset <math>U(r)</math> and a closed subset <math>V(r)</math> of <math>X</math> such that:
* <math>A \subseteq U(r)</math> and <math>V(r)\subseteq B^\complement</math> for all <math>r</math>,
* <math>U(r)\subseteq V(r)</math> for all <math>r</math>,
* For <math>r < s</math>, <math>V(r)\subseteq U(s)</math>.
Intuitively, the sets <math>U(r)</math> and <math>V(r)</math> expand outwards in layers from <math>A</math>:

: <math>\begin{array}{ccccccccccccccc}
A&&&&&&&\subseteq&&&&&&& B^\complement\\
A&&&\subseteq&&&\ U(1/2)&\subseteq& V(1/2)&&&\subseteq&&& B^\complement\\
A&\subseteq& U(1/4)&\subseteq& V(1/4)&\subseteq& U(1/2)&\subseteq& V(1/2)&\subseteq& U(3/4)&\subseteq& V(3/4)&\subseteq& B^\complement
\end{array}</math>

This construction proceeds by [[mathematical induction]]. For the base step, we define two extra sets <math>U(1) = B^\complement</math> and <math>V(0) = A </math>. 

Now assume that <math>n \geq 0</math> and that the sets <math>U\left(k/2^n\right)</math> and <math>V\left(k/2^n\right)</math> have already been constructed for <math>k \in\{ 1, \ldots, 2^n - 1\}</math>. Note that this is [[Vacuous truth|vacuously]] satisfied for <math>n=0</math>. Since <math>X</math> is normal, for any <math>a \in \left\{ 0, 1, \ldots, 2^n - 1 \right\}</math>, we can find an open set and a closed set such that

: <math>V\left(\frac{a}{2^n}\right)\subseteq U\left(\frac{2a+1}{2^{n+1}}\right)\subseteq V\left(\frac{2a+1}{2^{n+1}}\right)\subseteq U\left(\frac{a+1}{2^n}\right)</math>

The above three conditions are then verified.

Once we have these sets, we define <math>f(x) = 1</math> if <math>x \not\in U(r)</math> for any <math>r</math>; otherwise <math>f(x) = \inf \{ r : x \in U(r) \}</math> for every <math>x \in X</math>, where <math>\inf</math> denotes the [[infimum]]. Using the fact that the dyadic rationals are [[Dense set|dense]], it is then not too hard to show that <math>f</math> is continuous and has the property <math>f(A) \subseteq \{ 0 \}</math> and <math>f(B) \subseteq \{ 1 \}.</math> This step requires the <math>V(r)</math> sets in order to work.

The [[Mizar system|Mizar project]] has completely formalised and automatically checked a proof of Urysohn's lemma in the [http://mizar.org/JFM/Vol13/urysohn3.html URYSOHN3 file].