4.1. The converse🔗

Let us first see the proof of the converse, which is easier.

Proof. Suppose that any pair of disjoint closed sets of X can be separated by a continuous function, and let us see that then X is a normal space. Let C_1 and C_2 be disjoint closed sets in X.

intro hmprX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}⊢ NormalSpace X
rw [normal_space_def]mprX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}⊢ ∀ (C D : Set X), IsClosed C → IsClosed D → Disjoint C D → ∃ U V, IsOpen U ∧ IsOpen V ∧ C ⊆ U ∧ D ⊆ V ∧ Disjoint U V -- `1`
intro C1 C2mprX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set X⊢ IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ U V, IsOpen U ∧ IsOpen V ∧ C1 ⊆ U ∧ C2 ⊆ V ∧ Disjoint U V hC1mprX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1⊢ IsClosed C2 → Disjoint C1 C2 → ∃ U V, IsOpen U ∧ IsOpen V ∧ C1 ⊆ U ∧ C2 ⊆ V ∧ Disjoint U V hC2mprX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2⊢ Disjoint C1 C2 → ∃ U V, IsOpen U ∧ IsOpen V ∧ C1 ⊆ U ∧ C2 ⊆ V ∧ Disjoint U V hintermprX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2⊢ ∃ U V, IsOpen U ∧ IsOpen V ∧ C1 ⊆ U ∧ C2 ⊆ V ∧ Disjoint U V -- `2`

Since in the definition of normal we do not ask the closed sets to be non-empty, we have to distinguish these cases. However, these cases are trivial because it suffices to take the empty set to cover the empty set and X to cover the other set. In Lean we have to be rigorous with this step, but here we will skip it for simplicity.

Suppose, then, that C_1 and C_2 are non-empty. By hypothesis, there exists a continuous function f : X \to [0, 1] such that f(C_1) = \{0\} and f(C_2) = \{1\}.

obtain ⟨f, hf, hfC1, hfC2⟩ := h C1 C2 hC1nempty hC2nempty hC1 hC2 hintermpr.inr.inrX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:Continuous fhfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ ∃ U V, IsOpen U ∧ IsOpen V ∧ C1 ⊆ U ∧ C2 ⊆ V ∧ Disjoint U V

Consider then the sets U_1 = f^{-1}([0, \frac{1}{2})) and U_2 = f^{-1}((\frac{1}{2}, 1]). We want to see that they are the open sets we need for the definition of normal, that is, that they are open in X, that C_i \subseteq U_i and that they are disjoint.

use f ⁻¹' ({y | (y : ℝ) ∈ Set.Ico 0 (1 / 2)})hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:Continuous fhfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ ∃ V,
  IsOpen (f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)}) ∧
    IsOpen V ∧ C1 ⊆ f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)} ∧ C2 ⊆ V ∧ Disjoint (f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)}) V
use f ⁻¹' ({y | (y : ℝ) ∈ Set.Ioc (1 / 2) 1})hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:Continuous fhfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ IsOpen (f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)}) ∧
  IsOpen (f ⁻¹' {y | ↑y ∈ Set.Ioc (1 / 2) 1}) ∧
    C1 ⊆ f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)} ∧
      C2 ⊆ f ⁻¹' {y | ↑y ∈ Set.Ioc (1 / 2) 1} ∧
        Disjoint (f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)}) (f ⁻¹' {y | ↑y ∈ Set.Ioc (1 / 2) 1})

To see that U_1 is open, we use that f is continuous. It suffices to see that [0, \frac{1}{2}) is open in [0, 1]. But we already saw that intervals of the form [0, b) are open in [0, 1], so it suffices to apply that property. Analogous for U_2.

·h.leftX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ IsOpen (f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)}) apply hfh.left.aX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ IsOpen {y | ↑y ∈ Set.Ico 0 (1 / 2)} -- aplicar def. de f continua
  apply ico_open_in_Icc01h.left.a.hYX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ Y = Set.Icc 0 1h.left.a.hRX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ R = TopoSubspace UsualTopology Yh.left.a.hbX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ 0 < 1 / 2 ∧ 1 / 2 < 1 -- `[0, 1/2)` es abierto en `[0, 1]`
  ·h.left.a.hYX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ Y = Set.Icc 0 1 exact hYAll goals completed! 🐙
  ·h.left.a.hRX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ R = TopoSubspace UsualTopology Y exact hRAll goals completed! 🐙
  ·h.left.a.hbX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ 0 < 1 / 2 ∧ 1 / 2 < 1 norm_numAll goals completed! 🐙

To see that C_1 \subseteq U_1, it suffices to see that f(C_1) \subseteq [0, \frac{1}{2}), which is trivial. Analogous for U_2.

·h.right.right.leftX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ C1 ⊆ f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)} rw [← Set.image_subset_iff, hfC1]h.right.right.leftX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ {⟨0, ⋯⟩} ⊆ {y | ↑y ∈ Set.Ico 0 (1 / 2)} -- `{0} ⊆ [0, 1/2)` ?
  simpAll goals completed! 🐙

To see that they are disjoint, we see that [0, \frac{1}{2}) and (\frac{1}{2}, 1] are disjoint. Obviously they are, but for Lean it is a bit more complicated, so we proceed by contradiction in order to simplify the expressions. Finally we arrive at the fact that there is no x with x < 1/2 and x > 1/2.

·h.right.right.right.rightX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ Disjoint (f ⁻¹' {y | ↑y ∈ Set.Ico 0 (1 / 2)}) (f ⁻¹' {y | ↑y ∈ Set.Ioc (1 / 2) 1}) apply Disjoint.preimageh.right.right.right.right.hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}⊢ Disjoint {y | ↑y ∈ Set.Ico 0 (1 / 2)} {y | ↑y ∈ Set.Ioc (1 / 2) 1}
  by_contra ch.right.right.right.right.hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}c:¬Disjoint {y | ↑y ∈ Set.Ico 0 (1 / 2)} {y | ↑y ∈ Set.Ioc (1 / 2) 1}⊢ False
  apply (not_iff_not.mpr (Set.disjoint_iff_inter_eq_empty)).mp at ch.right.right.right.right.hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}c:¬{y | ↑y ∈ Set.Ico 0 (1 / 2)} ∩ {y | ↑y ∈ Set.Ioc (1 / 2) 1} = ∅⊢ False
  rw [← ne_eq, ← Set.nonempty_iff_ne_empty] at ch.right.right.right.right.hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}c:({y | ↑y ∈ Set.Ico 0 (1 / 2)} ∩ {y | ↑y ∈ Set.Ioc (1 / 2) 1}).Nonempty⊢ False
  obtain ⟨x, hxu, hxv⟩ := ch.right.right.right.right.hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}x:↑Yhxu:x ∈ {y | ↑y ∈ Set.Ico 0 (1 / 2)}hxv:x ∈ {y | ↑y ∈ Set.Ioc (1 / 2) 1}⊢ False
  simp at hxu hxvh.right.right.right.right.hX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace UsualTopology Yh:∀ (C1 C2 : Set X),
  C1 ≠ ∅ →
    C2 ≠ ∅ → IsClosed C1 → IsClosed C2 → Disjoint C1 C2 → ∃ f, Continuous f ∧ f '' C1 = {⟨0, ⋯⟩} ∧ f '' C2 = {⟨1, ⋯⟩}C1:Set XC2:Set XhC1:IsClosed C1hC2:IsClosed C2hinter:Disjoint C1 C2hC1nempty:C1 ≠ ∅hC2nempty:C2 ≠ ∅f:X → ↑Yhf:∀ (s : Set ↑Y), IsOpen s → IsOpen (f ⁻¹' s)hfC1:f '' C1 = {⟨0, ⋯⟩}hfC2:f '' C2 = {⟨1, ⋯⟩}x:↑Yhxu:0 ≤ ↑x ∧ ↑x < 2⁻¹hxv:2⁻¹ < ↑x ∧ ↑x ≤ 1⊢ False
  linarithAll goals completed! 🐙

∎

The other implication is much more complex, especially in its Lean formalisation, as we will see next.