Formalising Mathematics with Lean

4.5.Β The proofπŸ”—

We are going to prove, therefore, the main implication of Urysohn's lemma, following the Lean proof step by step.

Let X be a normal space. We want to prove that for each pair of non-empty disjoint closed sets C_1 and C_2 there exists a continuous function f : X \to [0, 1] such that f(C_1) = \{0\} and f(C_2) = \{1\}.

Let, then, C_1 and C_2 be closed sets with those conditions.

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, β‹―βŸ©} -- β†’ intro hT X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:NormalSpace XC1:Set X⊒ βˆ€ (C2 : Set X), C1 β‰  βˆ… β†’ C2 β‰  βˆ… β†’ IsClosed C1 β†’ IsClosed C2 β†’ Disjoint C1 C2 β†’ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:NormalSpace XC1:Set XC2:Set X⊒ C1 β‰  βˆ… β†’ C2 β‰  βˆ… β†’ IsClosed C1 β†’ IsClosed C2 β†’ Disjoint C1 C2 β†’ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:NormalSpace XC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…βŠ’ C2 β‰  βˆ… β†’ IsClosed C1 β†’ IsClosed C2 β†’ Disjoint C1 C2 β†’ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:NormalSpace XC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…βŠ’ IsClosed C1 β†’ IsClosed C2 β†’ Disjoint C1 C2 β†’ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:NormalSpace XC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1⊒ IsClosed C2 β†’ Disjoint C1 C2 β†’ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:NormalSpace XC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2⊒ Disjoint C1 C2 β†’ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:NormalSpace XC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2⊒ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©}

To begin with, we prove some auxiliary properties, such as that C_2^c is open (since C_2 is closed), and that C_1 \subseteq C_2^c (since they are disjoint), which will make it easier to apply the rest of the results we have been proving. We will also use the characterisation of normal spaces (3.14) on the hypothesis that X is normal.

have C2c_open : IsOpen C2ᢜ := 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, β‹―βŸ©} All goals completed! πŸ™ have hC1C2 : C1 βŠ† C2ᢜ := 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, β‹―βŸ©} All goals completed! πŸ™ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜ⊒ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©}

Now, for convenience we are going to define the following functions.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2⊒ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 x⊒ βˆƒ f, Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©}

This way we do not have to drag the arguments of H and k along at every step. I rename H to G to keep the notation of the outline, since it is the function of the form G : \mathbb{N} \to \mathcal{P}(X). I also rename k to g, to avoid confusion.

Now, recall that k : X \to \mathbb{R} was not exactly the function we were looking for. We are finally going to define the function to use to separate our closed sets, f, in the following way:

let f : X β†’ Y := fun x ↦ ⟨g x, X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xx:X⊒ g x ∈ Y X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xx:X⊒ g x ∈ Set.Icc 0 1 All goals completed! πŸ™βŸ©

That is, f is a function that takes values in X and returns a real value together with a proof that this value is actually in the interval [0, 1], given using k_in_01, which we had proved before. Therefore, Lean interprets it as a function f : X \to [0, 1], which is exactly what we wanted.

So we already have the separating function and we can take the big step:

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©βŠ’ Continuous f ∧ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©}

It remains to prove that f is continuous, that f(C_1) = \{0\} and that f(C_1) = \{1\}.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©βŠ’ Continuous fX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©βŠ’ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©}

4.5.1.Β Continuity of fπŸ”—

We want to see that f is continuous. To do so, we apply the result continuousInSubspace_iff_trueForBase, which we saw was a combination of 3.12 and 3.13.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©βŠ’ Continuous f X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©βŠ’ βˆ€ U ∈ {s | βˆƒ a b, s = Set.Ioo a b}, IsOpen (f ⁻¹' Subtype.val ⁻¹' U)

So it suffices to prove that for each basic open set W of \mathbb{R}, f^{-1}(W) is open in X. Let W = (a, b) be an open set of the base formed by the real open intervals.

intro W X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝhW:W ∈ {s | βˆƒ a b, s = Set.Ioo a b}⊒ IsOpen (f ⁻¹' Subtype.val ⁻¹' W) X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a b⊒ IsOpen (f ⁻¹' Subtype.val ⁻¹' W)

We want to see that f^{-1}(W) is open in X. Using the characterisation of open sets (3.1), it suffices to see that it is a neighbourhood of all of its points. Let then x \in f^{-1}(W), which means that f(x) \in (a, b).

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a b⊒ βˆ€ x ∈ f ⁻¹' Subtype.val ⁻¹' W, Neighbourhood (f ⁻¹' Subtype.val ⁻¹' W) x intro x X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:x ∈ f ⁻¹' Subtype.val ⁻¹' W⊒ Neighbourhood (f ⁻¹' Subtype.val ⁻¹' W) x X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a b⊒ Neighbourhood (f ⁻¹' Subtype.val ⁻¹' W) x

Since f(x) \in (a, b), there exists p \in \mathbb{Q} with a < p < f(x), and there also exists q \in \mathbb{Q} with f(x) < q < b.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)⊒ Neighbourhood (f ⁻¹' Subtype.val ⁻¹' W) x X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < b⊒ Neighbourhood (f ⁻¹' Subtype.val ⁻¹' W) x

We are going to prove that x \in G(q) and that x \notin \overline{G(p)}.

First let us recall the results 4.13 and 4.14 (with the function names corresponding to the current notation):

  • k_claim1: \forall p \in \mathbb{Q},\forall x \in X, x \in \overline{G(p)} \implies g(x) \leq p

  • k_claim2: \forall p \in \mathbb{Q},\forall x \in X, x \notin G(p) \implies g(x) \geq p

have claim1 := k_claim1 hT C1 C2 C1closed (X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < b⊒ IsOpen C2ᢜ All goals completed! πŸ™) (X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < b⊒ C1 βŠ† C2ᢜ All goals completed! πŸ™) have claim2 := k_claim2 hT C1 C2 C1closed (X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑p⊒ IsOpen C2ᢜ All goals completed! πŸ™) (X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑p⊒ C1 βŠ† C2ᢜ All goals completed! πŸ™)

(1) To see that x \notin \overline{G(p)}, suppose by contradiction that it is. Then we can apply claim1 and obtain that g(x) \leq p, but we had p < f(x) = g(x), contradiction.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑p⊒ x βˆ‰ closure (G p)X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)⊒ Neighbourhood (f ⁻¹' Subtype.val ⁻¹' W) x X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑p⊒ x βˆ‰ closure (G p) X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑pc:x ∈ closure (G p)⊒ False X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑pc:k hT C1 C2 x ≀ ↑p⊒ False All goals completed! πŸ™

(2) Similarly, if we suppose by contradiction that x \notin U(q), then by claim2 we obtain that g(x) \geq q, but we had q > f(x) = g(x), contradiction.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)⊒ x ∈ G qX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ Neighbourhood (f ⁻¹' Subtype.val ⁻¹' W) x X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)⊒ x ∈ G q X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)c:x βˆ‰ G q⊒ False X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)c:k hT C1 C2 x β‰₯ ↑q⊒ False All goals completed! πŸ™

Recapping, we want to see that f^{-1}(W) is a neighbourhood of x (x was arbitrary). This is, by definition, finding a set U\subseteq X that is open and such that x \in U \subseteq f^{-1}(W).

Let us take the set U = G(q) \cap (\overline{G(p)})^c and see that it satisfies these conditions.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ G q ∩ (closure (G p))ᢜ βŠ† f ⁻¹' Subtype.val ⁻¹' W ∧ OpenNeighbourhood (G q ∩ (closure (G p))ᢜ) x X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ G q ∩ (closure (G p))ᢜ βŠ† f ⁻¹' Subtype.val ⁻¹' WX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ OpenNeighbourhood (G q ∩ (closure (G p))ᢜ) x

(1) Let us see that U \subseteq f^{-1}(W). To do so, let y \in U and let us see that y \in f^{-1}(W) = f^{-1}((a, b)), that is, let us see that a < f(y) < b.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ G q ∩ (closure (G p))ᢜ βŠ† f ⁻¹' Subtype.val ⁻¹' W intro y X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ y ∈ f ⁻¹' Subtype.val ⁻¹' W X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ y ∈ f ⁻¹' Subtype.val ⁻¹' Set.Ioo a b X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ a < ↑(f y)X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ ↑(f y) < b

We have that y \notin G(p), since otherwise, y \in G(p) \subseteq \overline{G(p)}, but y \in \overline{G(p)}^c. Applying claim1, we have that f(y) = g(y) \geq p > a.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ a < ↑(f y) X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ y βˆ‰ G pX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy✝:y ∈ G q ∩ (closure (G p))ᢜhy:y βˆ‰ G p⊒ a < ↑(f y) X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ y βˆ‰ G p X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜc:y ∈ G p⊒ False X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜc:y ∈ closure (G p)⊒ False All goals completed! πŸ™ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy✝:y ∈ G q ∩ (closure (G p))ᢜhy:k hT C1 C2 y β‰₯ ↑p⊒ a < ↑(f y) All goals completed! πŸ™

On the other hand, since y \in G(q) \subseteq \overline{G(q)}, by claim2 we have that f(y) = g(y) \leq q < b.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy:y ∈ G q ∩ (closure (G p))ᢜ⊒ ↑(f y) < b X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy✝:y ∈ G q ∩ (closure (G p))ᢜhy:y ∈ G q⊒ ↑(f y) < b X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy✝:y ∈ G q ∩ (closure (G p))ᢜhy:y ∈ closure (G q)⊒ ↑(f y) < b X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G qy:Xhy✝:y ∈ G q ∩ (closure (G p))ᢜhy:y ∈ closure (G q)claim1:k hT C1 C2 y ≀ ↑q⊒ ↑(f y) < b All goals completed! πŸ™

So we conclude that f(y) \in (a, b) = W. The hard work is already done; it only remains to see that x \in U and that U is open.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ x ∈ G q ∩ (closure (G p))ᢜX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ IsOpen (G q ∩ (closure (G p))ᢜ)

(2) As we had seen, x \in G(q) and x \notin \overline{G(p)}. Hence x \in U.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ x ∈ G q ∩ (closure (G p))ᢜ -- probar que `x ∈ V` X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ x ∈ G qX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ x ∈ (closure (G p))ᢜ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ x ∈ G q All goals completed! πŸ™ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ x ∈ (closure (G p))ᢜ All goals completed! πŸ™

(3) Proving that U is open is easy: since it is a finite intersection, it suffices to see that both components are open. By 4.5, G(q) is open. Moreover, \overline{G(p)} is closed for being a closure, so its complement is open.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ IsOpen (G q ∩ (closure (G p))ᢜ) -- probar que `V` es abierto X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ IsOpen (G q)X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ IsOpen (closure (G p))ᢜ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ IsOpen (G q) All goals completed! πŸ™ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ IsOpen (closure (G p))ᢜ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©W:Set ℝa:ℝb:ℝhW:W = Set.Ioo a bx:Xhx:f x ∈ Subtype.val ⁻¹' Set.Ioo a bp:β„šhp:a < ↑p ∧ ↑p < ↑(f x)q:β„šhq:↑(f x) < ↑q ∧ ↑q < bclaim1:βˆ€ (p : β„š), βˆ€ x ∈ closure (H hT C1 C2 p), k hT C1 C2 x ≀ ↑pclaim2:βˆ€ (p : β„š), βˆ€ x βˆ‰ H hT C1 C2 p, k hT C1 C2 x β‰₯ ↑paux1:x βˆ‰ closure (G p)aux2:x ∈ G q⊒ IsClosed (closure (G p)) All goals completed! πŸ™

4.5.2.Β Image of fπŸ”—

To finish the proof, it only remains to see that f(C_1) = \{0\} and that f(C_2) = \{1\}.

To begin with, note that f(A) = g(A) for any A \subseteq X.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©βŠ’ βˆ€ (A : Set X), Subtype.val '' f '' A = g '' AX:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©aux:βˆ€ (A : Set X), Subtype.val '' f '' A = g '' A⊒ f '' C1 = {⟨0, β‹―βŸ©} ∧ f '' C2 = {⟨1, β‹―βŸ©} X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©βŠ’ βˆ€ (A : Set X), Subtype.val '' f '' A = g '' A X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©A:Set X⊒ Subtype.val '' f '' A = g '' A; X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©A:Set Xx:β„βŠ’ x ∈ Subtype.val '' f '' A ↔ x ∈ g '' A; All goals completed! πŸ™

So we can reduce the goal to g(C_1) = \{0\} and g(C_2) = \{1\}.

The result then follows from lemma 4.18 and its analogue for C_2.

X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©aux:βˆ€ (A : Set X), Subtype.val '' f '' A = g '' A⊒ g '' C1 = {0}X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©aux:βˆ€ (A : Set X), Subtype.val '' f '' A = g '' A⊒ g '' C2 = {1} /- 2. f(C1) = {0} -/ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©aux:βˆ€ (A : Set X), Subtype.val '' f '' A = g '' A⊒ g '' C1 = {0} All goals completed! πŸ™ /- 3. f(C2) = {1} -/ X:TypeY:Set ℝT:TopologicalSpace XT':TopologicalSpace ℝhT':T' = UsualTopologyR:TopologicalSpace ↑YhY:Y = Set.Icc 0 1hR:R = TopoSubspace T' YhT:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1nempty:C1 β‰  βˆ…C2nempty:C2 β‰  βˆ…C1closed:IsClosed C1C2closed:IsClosed C2C1C2disj:Disjoint C1 C2C2c_open:IsOpen C2ᢜhC1C2:C1 βŠ† C2ᢜG:β„š β†’ Set X := H hT C1 C2g:X β†’ ℝ := fun x => k hT C1 C2 xf:X β†’ ↑Y := fun x => ⟨g x, β‹―βŸ©aux:βˆ€ (A : Set X), Subtype.val '' f '' A = g '' A⊒ g '' C2 = {1} All goals completed! πŸ™

Which concludes the proof of Urysohn's lemma.