Theorem 4.1 (Urysohn's Lemma)
(Stephen Willard, 2012)Stephen Willard, 2012. “General topology”. Courier Corporation. (p. 102, 15.6. Urysohn's Lemma).
Let (X, \mathcal{T}) be a topological space. X is a normal space if and only if for each pair of disjoint closed sets C and D in X, there exists a function f : X \to [0, 1] such that f(C) = \{0\} and f(D) = \{1\}.
For the formalisation in Lean, we will require the closed sets C and D to be non-empty. Obviously, if one of the two is empty, it suffices to take the continuous function f(x) \equiv 1, but we can discard these trivial cases.
lemma Urysohn {X : Type} {Y : Set ℝ}
(T : TopologicalSpace X)
[T' : TopologicalSpace ℝ]
(hT' : T' = UsualTopology)
{R : TopologicalSpace Y}
{hY : Y = Set.Icc 0 1}
{hR : R = TopoSubspace T' Y} :
NormalSpace X ↔
∀ C1 : Set X, ∀ C2 : Set X,
C1 ≠ ∅ → C2 ≠ ∅ →
IsClosed C1 → IsClosed C2 →
Disjoint C1 C2 →
∃ f : X → Y,
Continuous f ∧
f '' C1 = ({⟨0, X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YC1:Set XC2:Set Xf:X → ↑Y⊢ 0 ∈ Y All goals completed! 🐙⟩} : Set Y) ∧
f '' C2 = ({⟨1, X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YC1:Set XC2:Set Xf:X → ↑Y⊢ 1 ∈ Y All goals completed! 🐙⟩} : Set Y) := X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Y⊢ NormalSpace X ↔
∀ (C1 C2 : Set X),
C1 ≠ ∅ →
C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}