4.4. Construction of a separating continuous function🔗

Continuing with the outline we had proposed, we now construct the following function

\begin{array}{rcrcl} F & : & X & \longrightarrow & \mathcal{P}(\mathbb{Q}) \\ & & x & \longmapsto & \{p \in \mathbb{Q} ~|~ x \in H(p)\} \end{array}

def F {X : Type} [TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)

    (C1 C2 : Set X)

    : X → Set ℚ := fun x : X ↦ {p : ℚ | x ∈ H hT C1 C2 p}

Now, we want to construct a function of the following form

\begin{array}{rcrcl} f & : & X & \longrightarrow & [0, 1] \\ & & x & \longmapsto & \inf F(x) \end{array}

However, we have to make sure that we can define this function, that is, that the set F(x) has an infimum for each x \in X.

4.4.1. The function `F`🔗

Lemma 4.9🔗

Let F : X \to \mathcal{P}(\mathbb{Q}) be the function defined above. Then for each x \in X, F(x) is a non-empty set.

Proof. Let x \in X. Any q > 1 is such that q \in F(x), since if q >1, H(q) = X, hence x \in H(q). ∎

lemma hF_non_empty {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    :  ∀ x : X, (F hT C1 C2 x).Nonempty := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set X⊢ ∀ (x : X), (F hT C1 C2 x).Nonempty
  intro xX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:X⊢ (F hT C1 C2 x).Nonempty
  use 2hX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:X⊢ 2 ∈ F hT C1 C2 x
  simp [F, H]All goals completed! 🐙

Lemma 4.10🔗

For each x \in X, if q < 0 then q \notin F(x). That is, all the elements of F(x) are non-negative.

Proof. Let x \in X and q < 0. Then H(q) = \emptyset, hence obviously x \notin H(q). ∎

We will call this result hFx_non_neg. As a consequence, we have:

Lemma 4.11🔗

For each x \in X, 0 is a lower bound of F(x).

lemma hFx_has_lb_0 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    : ∀ x : X, 0 ∈ lowerBounds (F hT C1 C2 x) := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set X⊢ ∀ (x : X), 0 ∈ lowerBounds (F hT C1 C2 x)

Therefore, given x \in X, since F(x) is a non-empty set bounded from below, we can conclude that F(x) has an infimum as a real set, that is, we can conclude that there exists a number r \in \mathbb{R} such that r = \inf F(x). This result is included in Mathlib:

theorem Real.exists_isGLB {s : Set ℝ} (hne : s.Nonempty) (hbdd : BddBelow s) :
    ∃ x, IsGLB s x

We could try to write something like this:

  lemma hFx_has_lb_0 (...)
    : ∀ x : X, ∃ r : ℝ, IsGLB (F hT C1 C2 x) r := by sorry

However, this gives us the following error:

  argument r has type ℝ but is expected to have type ℚ

This is because, in Mathlib, IsGLB is defined in the following way:

def IsGLB [Preorder α] (s : Set α) : α → Prop :=
  IsGreatest (lowerBounds s)

That is, it is only defined for values of type \alpha if s \subset \alpha. Since F(x) \subset \mathbb{Q}, we cannot say that r \in \mathbb{R} is its infimum.

Therefore, we need to define in Lean an auxiliary function \tilde{F} such that \tilde{F}(x) = F(x) for each x, but seen as a subset of \mathbb{R}. We do it in the following way.

def inclQR : ℚ → ℝ := fun q ↦ q

def F_Real {X : Type} [TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    : X → Set ℝ :=

    fun x ↦ inclQR '' (F hT C1 C2 x)

This new function \tilde{F} is a function with the same properties as F, that is, for each x \in X, \tilde{F}(x) is a non-empty set with 0 as a lower bound. This is proved immediately using the properties of F, although it is necessary to be careful with Lean's type inference in some cases.

But now \tilde{F} returns subsets of \mathbb{R}, so we can assert that it has an infimum in \mathbb{R}.

lemma F_Real_has_inf {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    : ∀ x : X, ∃ r : ℝ, IsGLB (F_Real hT C1 C2 x) r := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set X⊢ ∀ (x : X), ∃ r, IsGLB (F_Real hT C1 C2 x) r

  intro xX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:X⊢ ∃ r, IsGLB (F_Real hT C1 C2 x) r
  apply Real.exists_isGLBhneX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:X⊢ (F_Real hT C1 C2 x).NonemptyhbddX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:X⊢ BddBelow (F_Real hT C1 C2 x)
  exact F_Real_Nonempty hT C1 C2 xhbddX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:X⊢ BddBelow (F_Real hT C1 C2 x)
  exact F_Real_BddBelow hT C1 C2 xAll goals completed! 🐙

4.4.2. The function `f`🔗

Once we have made sure that \tilde{F} has an infimum, we can try to define our function f as we wanted. Before that, let us make the following remark.

We want to find a function f : X \to [0, 1]. However, we have only guaranteed that \inf \tilde{F}(x) \in \mathbb{R}; not necessarily \inf \tilde{F}(x) \in [0, 1].

Evidently, the latter is true, because 0 is a lower bound, so the infimum will be at least 0, and \forall q>1, q \in F(x), so the infimum cannot be greater than 1.

However, for ease of working with Lean, we will first define a function that is simply

\begin{array}{rcrcl} k & : & X & \longrightarrow & \mathbb{R} \\ & & x & \longmapsto & \inf \tilde{F}(x) \end{array}

and we prove that indeed k(x) \in [0, 1] for each x\in X. Later, we will use the function f(x) = k(x), taking care to specify that k(x) \in [0, 1].

noncomputable def k {X : Type} [TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    : X → ℝ :=
    fun x ↦ Classical.choose (F_Real_has_inf hT C1 C2 x)

We obtain the following property, the result of applying Classical.choose_spec to k.

lemma k_prop {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    : ∀ x, IsGLB (F_Real hT C1 C2 x) (k hT C1 C2 x) := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set X⊢ ∀ (x : X), IsGLB (F_Real hT C1 C2 x) (k hT C1 C2 x)

Lemma 4.12🔗

For each x \in X, the function k : X \to \mathbb{R} we have just defined satisfies k(x) \in [0, 1].

lemma k_in_01 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    : ∀ x : X, (k hT C1 C2 x) ∈ Set.Icc 0 1 := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set X⊢ ∀ (x : X), k hT C1 C2 x ∈ Set.Icc 0 1

Proof. The proof is easy and we have already explained it, but in Lean we need to give a complete specification, so we explain it.

Let x \in X. Recall that k(x) is a lower bound of \tilde{F}(x) (klb) and it is the greatest of them (kglb).

intro xX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:X⊢ k hT C1 C2 x ∈ Set.Icc 0 1
have ⟨klb, kglb⟩ := k_prop hT C1 C2 xX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))⊢ k hT C1 C2 x ∈ Set.Icc 0 1
constructorleftX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))⊢ 0 ≤ k hT C1 C2 xrightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))⊢ k hT C1 C2 x ≤ 1

Seeing that k(x) \geq 0 is easy, because we have already seen that 0 is a lower bound, and k(x) is the greatest one.

·leftX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))⊢ 0 ≤ k hT C1 C2 x exact kglb (F_Real_0_is_LB hT C1 C2 x)All goals completed! 🐙

Now, to see that k(x) \leq 1, we proceed by contradiction. Suppose that k(x) > 1. Then there exists a rational number q such that 1 < q < k(x). Since q > 1, we know that q \in \tilde{F}(x). But in that case, since k(x) is a lower bound, k(x) \leq q, which is contradictory.

·rightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))⊢ k hT C1 C2 x ≤ 1 by_contra crightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))c:¬k hT C1 C2 x ≤ 1⊢ False
  simp at crightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))c:1 < k hT C1 C2 x⊢ False
  obtain ⟨q, hq1, hqk⟩ := exists_rat_btwn crightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))c:1 < k hT C1 C2 xq:ℚhq1:1 < ↑qhqk:↑q < k hT C1 C2 x⊢ False
  have hq := F_Real_1inf hT C1 C2 x q (byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))c:1 < k hT C1 C2 xq:ℚhq1:1 < ↑qhqk:↑q < k hT C1 C2 x⊢ q > 1 exact_mod_cast hq1All goals completed! 🐙)
  apply klb at hqrightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))c:1 < k hT C1 C2 xq:ℚhq1:1 < ↑qhqk:↑q < k hT C1 C2 xhq:k hT C1 C2 x ≤ inclQR q⊢ False
  apply not_lt.mpr at hqrightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set Xx:Xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)kglb:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))c:1 < k hT C1 C2 xq:ℚhq1:1 < ↑qhqk:↑q < k hT C1 C2 xhq:¬inclQR q < k hT C1 C2 x⊢ False
  exact hq hqkAll goals completed! 🐙

∎

Finally, before moving on to the proof of Urysohn's lemma at last, we give several properties of k that we will need. Recall that H was G \circ f^{-1} extended to \mathbb{Q}.

Lemma 4.13🔗

For each p \in \mathbb{Q} and each x \in X, if x \in \overline{H(p)} then k(x) \leq p.

lemma k_claim1 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    (hC1 : IsClosed C1)
    (hC2 : IsOpen C2ᶜ)
    (hC1C2 : C1 ⊆ C2ᶜ)

    : ∀ p : ℚ, ∀ x : X, x ∈ closure (H hT C1 C2 p) → (k hT C1 C2 x) ≤ p := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜ⊢ ∀ (p : ℚ), ∀ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≤ ↑p

Proof. Let p \in \mathbb{Q} and x \in X with x \in \overline{H(p)}. Suppose, for contradiction, that k(x) > p. Then there exists a rational q \in \mathbb{Q} such that p < q < k(x).

intro p xX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:X⊢ x ∈ closure (H hT C1 C2 p) → k hT C1 C2 x ≤ ↑p hxX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xhx:x ∈ closure (H hT C1 C2 p)⊢ k hT C1 C2 x ≤ ↑p
by_contra cX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xhx:x ∈ closure (H hT C1 C2 p)c:¬k hT C1 C2 x ≤ ↑p⊢ False
simp at cX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xhx:x ∈ closure (H hT C1 C2 p)c:↑p < k hT C1 C2 x⊢ False
have ⟨q, hq⟩ := exists_rat_btwn cX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xhx:x ∈ closure (H hT C1 C2 p)c:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 x⊢ False

Since p < q and x \in \overline{H(p)}, by (★) we have that x \in H(q).

apply H_isOrdered hT C1 C2 hC1 hC2 hC1C2 p q
  (byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xhx:x ∈ closure (H hT C1 C2 p)c:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 x⊢ p < q exact_mod_cast hq.leftAll goals completed! 🐙)
  at hx

Now, x \in H(q) means that q \in \tilde{F}(x). But k(x) is a lower bound of \tilde{F}(x), hence k(x) < q, which contradicts q < k(x).

have aux : inclQR q ∈ F_Real hT C1 C2 xauxX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 q⊢ inclQR q ∈ F_Real hT C1 C2 xX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 qaux:inclQR q ∈ F_Real hT C1 C2 x⊢ False
·auxX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 q⊢ inclQR q ∈ F_Real hT C1 C2 x simp [F_Real]auxX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 q⊢ ∃ x_1 ∈ F hT C1 C2 x, inclQR x_1 = inclQR q
  use qhX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 q⊢ q ∈ F hT C1 C2 x ∧ inclQR q = inclQR q
  simphX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 q⊢ q ∈ F hT C1 C2 x
  exact hxAll goals completed! 🐙

have ⟨klb, _⟩ := k_prop hT C1 C2 xX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 qaux:inclQR q ∈ F_Real hT C1 C2 xklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)right✝:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))⊢ False
apply klb at auxX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 qklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)right✝:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))aux:k hT C1 C2 x ≤ inclQR q⊢ False
apply not_lt.mpr at auxX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜp:ℚx:Xc:↑p < k hT C1 C2 xq:ℚhq:↑p < ↑q ∧ ↑q < k hT C1 C2 xhx:x ∈ H hT C1 C2 qklb:k hT C1 C2 x ∈ lowerBounds (F_Real hT C1 C2 x)right✝:k hT C1 C2 x ∈ upperBounds (lowerBounds (F_Real hT C1 C2 x))aux:¬inclQR q < k hT C1 C2 x⊢ False
exact aux hq.rightAll goals completed! 🐙

∎

Lemma 4.14🔗

For each p \in \mathbb{Q} and each x \in X, if x \notin H(p) then k(x) \geq p.

lemma k_claim2 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    (hC1 : IsClosed C1)
    (hC2 : IsOpen C2ᶜ)
    (hC1C2 : C1 ⊆ C2ᶜ)

    : ∀ p : ℚ, ∀ x : X, x ∉ (H hT C1 C2 p) → (k hT C1 C2 x) ≥ p := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜ⊢ ∀ (p : ℚ), ∀ x ∉ H hT C1 C2 p, k hT C1 C2 x ≥ ↑p

Proof. The proof is very similar to the previous one and can be found in the repository. ∎

4.4.3. Properties on the closed sets `C_1` and `C_2`🔗

Finally, let us see how the function k behaves on the closed sets we want to separate. This will leave the path completely clear to complete the proof of Urysohn's lemma. We are going to see the proofs for C_1; the ones for C_2 are similar and can be checked in the repository.

We want to arrive at k(C_1) = \{0\}. This property is built step by step, using properties of the functions it relies on.

Lemma 4.15🔗

Consider F : X \to \mathcal{P}(\mathbb{Q}). For each x \in C_1, we have that F(x) = \{q \in \mathbb{Q} ~|~ q \geq 0\}.

lemma F_at_C1 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)

    (C1 C2 : Set X)
    (hC1 : IsClosed C1)
    (hC2 : IsOpen C2ᶜ)
    (hC1C2 : C1 ⊆ C2ᶜ)

    : ∀ x : X, x ∈ C1 → F hT C1 C2 x = {q : ℚ | q ≥ 0} := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜ⊢ ∀ x ∈ C1, F hT C1 C2 x = {q | q ≥ 0}

Proof. Let x \in C_1. Seeing that F(x) \subseteq \{q \in \mathbb{Q} ~|~ q \geq 0\} is easy, since we have already seen that no value of F(x) is negative (hFx_non_neg). Now, let q \geq 0 and let us see that q \in F(x), that is, that x \in H(q).

If q > 0, by the property (★) of H, \overline{H(0)} \subseteq H(q). And by the construction of H we have C_1 \subseteq H(0). Hence x \in H(q). If q = 0, since C_1 \subseteq H(0), x\in H(q).

·h.mprX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq:q ∈ {q | q ≥ 0}⊢ q ∈ F hT C1 C2 x simp only [ge_iff_le, Set.mem_setOf_eq] at hqh.mprX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq:0 ≤ q⊢ q ∈ F hT C1 C2 x
  cases' Decidable.lt_or_eq_of_le hq with hq hqh.mpr.inlX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq✝:0 ≤ qhq:0 < q⊢ q ∈ F hT C1 C2 xh.mpr.inrX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq✝:0 ≤ qhq:0 = q⊢ q ∈ F hT C1 C2 x

  ·h.mpr.inlX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq✝:0 ≤ qhq:0 < q⊢ q ∈ F hT C1 C2 x apply H_isOrdered hT C1 C2 hC1 hC2 hC1C2 0 q hqh.mpr.inl.aX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq✝:0 ≤ qhq:0 < q⊢ x ∈ closure (H hT C1 C2 0)
    apply subset_closureh.mpr.inl.a.aX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq✝:0 ≤ qhq:0 < q⊢ x ∈ H hT C1 C2 0
    exact H_C1_in_H0 hT C1 C2 hC1 hC2 hC1C2 hxAll goals completed! 🐙

  ·h.mpr.inrX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq✝:0 ≤ qhq:0 = q⊢ q ∈ F hT C1 C2 x rw [← hq]h.mpr.inrX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜx:Xhx:x ∈ C1q:ℚhq✝:0 ≤ qhq:0 = q⊢ 0 ∈ F hT C1 C2 x
    exact H_C1_in_H0 hT C1 C2 hC1 hC2 hC1C2 hxAll goals completed! 🐙

∎

Lemma 4.16🔗

Consider F : X \to \mathcal{P}(\mathbb{Q}). For each x \in C_1, we have that \inf{F}(x) = 0.

lemma F_0_GLB_in_C1 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)

    (C1 C2 : Set X)
    (hC1 : IsClosed C1)
    (hC2 : IsOpen C2ᶜ)
    (hC1C2 : C1 ⊆ C2ᶜ)

    : ∀ x : X, x ∈ C1 → IsGLB (F hT C1 C2 x) 0 := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜ⊢ ∀ x ∈ C1, IsGLB (F hT C1 C2 x) 0

Once we know that F(x) = \{q \in \mathbb{Q} ~|~ q \geq 0\}, seeing that the infimum of this set is 0 is direct. Note that here we can indeed define the infimum over F because 0 \in \mathbb{Q}. Now we can state the same for \tilde{F}, simply being careful with the type of F(x) and of 0.

Lemma 4.17🔗

Consider \tilde{F} : X \to \mathcal{P}(\mathbb{R}). For each x \in C_1, we have that \inf{\tilde{F}}(x) = 0.

lemma F_Real_0_GLB_in_C1 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)

    (C1 C2 : Set X)
    (hC1 : IsClosed C1)
    (hC2 : IsOpen C2ᶜ)
    (hC1C2 : C1 ⊆ C2ᶜ)

    : ∀ x : X, x ∈ C1 → IsGLB (F_Real hT C1 C2 x) 0 := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜ⊢ ∀ x ∈ C1, IsGLB (F_Real hT C1 C2 x) 0

Finally, we have:

Lemma 4.18🔗

Consider k : X \to \mathbb{R}. Recall that C_1 is non-empty. We have that k (C_1) = \{0\}.

lemma k_in_C1_is_0 {X : Type} [T : TopologicalSpace X]
    (hT : ∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ U)
    (C1 C2 : Set X)

    (hC1 : IsClosed C1)
    (hC2 : IsOpen C2ᶜ)
    (hC1C2 : C1 ⊆ C2ᶜ)
    (hC1_nonempty : C1 ≠ ∅)

    : k hT C1 C2 '' C1 = {0} := byX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅⊢ k hT C1 C2 '' C1 = {0}

Proof. To see that k(C_1) \subseteq \{0\}, since k(x) := \inf \tilde{F}(x), and \inf \tilde{F}(x) = 0 for x \in C_1 by the previous result, it suffices to use that the infimum is unique.

ext rhX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝ⊢ r ∈ k hT C1 C2 '' C1 ↔ r ∈ {0}
constructorh.mpX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝ⊢ r ∈ k hT C1 C2 '' C1 → r ∈ {0}h.mprX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝ⊢ r ∈ {0} → r ∈ k hT C1 C2 '' C1
·h.mpX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝ⊢ r ∈ k hT C1 C2 '' C1 → r ∈ {0} intro ⟨x, hx, hr⟩h.mpX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝx:Xhx:x ∈ C1hr:k hT C1 C2 x = r⊢ r ∈ {0}
  rw [← hr]h.mpX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝx:Xhx:x ∈ C1hr:k hT C1 C2 x = r⊢ k hT C1 C2 x ∈ {0}
  apply IsGLB.unique (k_prop hT C1 C2 x)h.mpX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝx:Xhx:x ∈ C1hr:k hT C1 C2 x = r⊢ IsGLB (F_Real hT C1 C2 x) 0
  exact F_Real_0_GLB_in_C1 hT C1 C2 hC1 hC2 hC1C2 x hxAll goals completed! 🐙

To see that \{0\} \subseteq k(x), we need to see that there exists an x \in C_1 such that k(x) = 0. Since C_1 is non-empty, let x \in C_1 be arbitrary. Then k(x) = 0, proceeding in the same way as in the first inclusion.

·h.mprX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝ⊢ r ∈ {0} → r ∈ k hT C1 C2 '' C1 intro hrh.mprX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}⊢ r ∈ k hT C1 C2 '' C1
  rw [hr]h.mprX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}⊢ 0 ∈ k hT C1 C2 '' C1
  obtain ⟨x, hx⟩ := nonempty_has_element C1 hC1_nonemptyh.mprX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1⊢ 0 ∈ k hT C1 C2 '' C1
  use xhX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1⊢ x ∈ C1 ∧ k hT C1 C2 x = 0
  constructorh.leftX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1⊢ x ∈ C1h.rightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1⊢ k hT C1 C2 x = 0
  ·h.leftX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1⊢ x ∈ C1 exact hxAll goals completed! 🐙
  ·h.rightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1⊢ k hT C1 C2 x = 0 have aux := F_Real_0_GLB_in_C1 hT C1 C2 hC1 hC2 hC1C2 x hxh.rightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1aux:IsGLB (F_Real hT C1 C2 x) 0⊢ k hT C1 C2 x = 0
    have aux' := Classical.choose_spec (F_Real_has_inf hT C1 C2 x)h.rightX:TypeT:TopologicalSpace XhT:∀ (U C : Set X), IsOpen U → IsClosed C → C ⊆ U → ∃ V, IsOpen V ∧ C ⊆ V ∧ closure V ⊆ UC1:Set XC2:Set XhC1:IsClosed C1hC2:IsOpen C2ᶜhC1C2:C1 ⊆ C2ᶜhC1_nonempty:C1 ≠ ∅r:ℝhr:r ∈ {0}x:Xhx:x ∈ C1aux:IsGLB (F_Real hT C1 C2 x) 0aux':IsGLB (F_Real hT C1 C2 x) (Classical.choose ⋯)⊢ k hT C1 C2 x = 0
    exact IsGLB.unique aux' auxAll goals completed! 🐙

∎