Formalising Mathematics with Lean

3.5.Β SeparationπŸ”—

Not every topology on a set adequately reflects the properties of that set. For example, the trivial topology does not allow us to tell elements of the space apart, so under this topology it is not possible to distinguish some sets from others or even from a single point.

To go deeper into the study of topology, certain conditions are introduced that guarantee that the points of the space can be distinguished in some way by means of open sets. These conditions are known as separation axioms.

For example, a space is Hausdorff if given two distinct points, there exist disjoint open sets containing each of them. This condition is true for any metric space, and guarantees certain nice properties, such as the uniqueness of limits.

In this work we will focus, in particular, on normal spaces.

3.5.1.Β Normal spacesπŸ”—

Normal spaces allow us to separate not only points, but disjoint closed sets by means of disjoint open sets. This property is more demanding, but also more powerful.

One of the most important properties of normal spaces is that they allow us to distinguish between closed sets by separating them with continuous functions, which is known as Urysohn's lemma. The formalisation of this result is one of the main objectives of this work.

Definition 3.10πŸ”—

Let X be a topological space. We will say that X is a normal space if for each pair of disjoint closed sets C, D \subseteq X there exist disjoint open sets U and V in X that separate C and D, that is, C \subseteq U and D \subseteq VIn Lean, the NormalSpace definition is slightly different, but it uses objects that we have not used. Instead, we use this one together with a proof that they are equivalent, which I have called normal_space_def..

def NormalSpace {X : Type} (T : TopologicalSpace X) : Prop := βˆ€ C : Set X, βˆ€ D : Set X, IsClosed C β†’ IsClosed D β†’ C ∩ D = βˆ… β†’ βˆƒ U : Set X, βˆƒ V : Set X, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ U ∩ V = βˆ…

Now we want to give a characterisation of this kind of space, which will make our work easier later on.

Proposition 3.14 (Characterisation of normal spaces)πŸ”—

Let X be a topological space. X is normal if and only if for each open U and each closed C of X such that C \subseteq U, there exists an open V \subset X such that C \subseteq V \subseteq \overline{V} \subseteq U.

lemma characterization_of_normal {X : Type} (T : TopologicalSpace X) : NormalSpace X ↔ βˆ€ U : Set X, βˆ€ C : Set X, IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V : Set X, IsOpen V ∧ C βŠ† V ∧ (closure V) βŠ† U := X:TypeT:TopologicalSpace X⊒ NormalSpace X ↔ βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U

Proof. Let us see each implication separately.

X:TypeT:TopologicalSpace X⊒ (βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U V) ↔ βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U X:TypeT:TopologicalSpace X⊒ (βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U V) β†’ βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UX:TypeT:TopologicalSpace X⊒ (βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) β†’ βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U V

(\implies) Suppose that X is a normal space (hT) and let U be an open set (hU) and C a closed set (hC) such that C \subseteq U (hCU).

X:TypeT:TopologicalSpace X⊒ (βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U V) β†’ βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U intro hT X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set X⊒ βˆ€ (C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set X⊒ IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen U⊒ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed C⊒ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† U⊒ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U

Since X is normal, by the definition, for C and U^c closed in X we obtain V_1 and V_2 open (V1_open, V2_open) and disjoint (hV) such that C \subseteq V_1 (hCV) and U^c \subseteq V_2 (hUV).

obtain ⟨V1, V2, V1_open, V2_open, hCV, hUV, hV⟩ := hT C Uᢜ hC (X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† U⊒ IsClosed Uᢜ All goals completed! πŸ™) (X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† U⊒ Disjoint C Uᢜ X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† U⊒ C βŠ† U; All goals completed! πŸ™)

Of course, in Lean we have to specify why U^c is closed and why U^c \subseteq V_2. We take as V the V_1 obtained in this way. We already know that V_1 is open and that C\subseteq V_1, so it only remains to prove that \overline{V_1} \subseteq U.

X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ IsOpen V1 ∧ C βŠ† V1 ∧ closure V1 βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ IsOpen V1X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ C βŠ† V1 ∧ closure V1 βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ IsOpen V1 All goals completed! πŸ™ X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ C βŠ† V1X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ closure V1 βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ C βŠ† V1 All goals completed! πŸ™

We know that U^c \subseteq V_2 (hUV), hence V_2^c \subseteq U. It suffices to see that \overline{V_1} \subseteq V_2^c.

But V_1 \cap V_2 = \emptyset \implies \overline{V_1} \cap V_2 = \emptyset, since V_2 is open. Hence \overline{V_1} \subseteq V_2^c.

X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ closure V1 βŠ† U X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ closure V1 βŠ† V2ᢜX:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ V2ᢜ βŠ† U; X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ V2ᢜ βŠ† UX:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ closure V1 βŠ† V2ᢜ X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ V2ᢜ βŠ† U All goals completed! πŸ™ X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint V1 V2⊒ closure V1 βŠ† V2ᢜ X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:IsOpen V2 β†’ Disjoint (closure V1) V2⊒ closure V1 βŠ† V2ᢜ X:TypeT:TopologicalSpace XhT:βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U VU:Set XC:Set XhU:IsOpen UhC:IsClosed ChCU:C βŠ† UV1:Set XV2:Set XV1_open:IsOpen V1V2_open:IsOpen V2hCV:C βŠ† V1hUV:Uᢜ βŠ† V2hV:Disjoint (closure V1) V2⊒ closure V1 βŠ† V2ᢜ All goals completed! πŸ™

(\impliedby) We proceed in a similar way. Let C_1 and C_2 be disjoint (hC) closed sets (C1_closed, C2_closed). We can apply the hypothesis (h) to the open set C_1^c and the closed set C_2 to obtain an open V (V_open) such that C_2 \subseteq V \subseteq \overline{V} \subseteq C_1^c (hV).

X:TypeT:TopologicalSpace X⊒ (βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† U) β†’ βˆ€ (C D : Set X), IsClosed C β†’ IsClosed D β†’ Disjoint C D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C βŠ† U ∧ D βŠ† V ∧ Disjoint U V intro h X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set X⊒ βˆ€ (D : Set X), IsClosed C1 β†’ IsClosed D β†’ Disjoint C1 D β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C1 βŠ† U ∧ D βŠ† V ∧ Disjoint U V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set X⊒ IsClosed C1 β†’ IsClosed C2 β†’ Disjoint C1 C2 β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C1 βŠ† U ∧ C2 βŠ† V ∧ Disjoint U V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1⊒ IsClosed C2 β†’ Disjoint C1 C2 β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C1 βŠ† U ∧ C2 βŠ† V ∧ Disjoint U V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2⊒ Disjoint C1 C2 β†’ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C1 βŠ† U ∧ C2 βŠ† V ∧ Disjoint U V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2⊒ βˆƒ U V, IsOpen U ∧ IsOpen V ∧ C1 βŠ† U ∧ C2 βŠ† V ∧ Disjoint U V obtain ⟨V, V_open, hV⟩ := h C1ᢜ C2 (X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2⊒ IsOpen C1ᢜ All goals completed! πŸ™) C2_closed (X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2⊒ C2 βŠ† C1ᢜ X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2⊒ Disjoint C1 C2; All goals completed! πŸ™)

Now we take the open sets U_1 = \overline{V}^c and U_2 = V. We want to see that they satisfy the normality condition for C_1 and C_2, that is:

  IsOpen (closure V)ᢜ ∧ IsOpen V ∧ C1 βŠ† (closure V)ᢜ ∧ C2 βŠ† V ∧ Disjoint (closure V)ᢜ V

Indeed, both are open (\overline{V}^c for being the complement of a closure and V by construction).

X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ IsOpen (closure V)ᢜX:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ IsOpen V ∧ C1 βŠ† (closure V)ᢜ ∧ C2 βŠ† V ∧ Disjoint (closure V)ᢜ V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ IsOpen (closure V)ᢜ X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ IsClosed (closure V) All goals completed! πŸ™ X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ IsOpen VX:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ C1 βŠ† (closure V)ᢜ ∧ C2 βŠ† V ∧ Disjoint (closure V)ᢜ V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ IsOpen V All goals completed! πŸ™

Moreover, C_1 \subseteq \overline{V}^c is equivalent to \overline{V} \subseteq C_1^c, which is true by the construction of V, as is C_2 \subseteq V.

X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ C1 βŠ† (closure V)ᢜX:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ C2 βŠ† V ∧ Disjoint (closure V)ᢜ V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ C1 βŠ† (closure V)ᢜ X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ closure V βŠ† C1ᢜ All goals completed! πŸ™ X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ C2 βŠ† VX:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ Disjoint (closure V)ᢜ V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ C2 βŠ† V All goals completed! πŸ™

Finally, we have \overline{V}^c \cap V = \emptyset \iff V \cap \overline{V}^c = \emptyset \iff V \subseteq \overline{V}^{cc} \iff V \subseteq \overline{V}, which is true by the properties of the closure.

X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ Disjoint (closure V)ᢜ V X:TypeT:TopologicalSpace Xh:βˆ€ (U C : Set X), IsOpen U β†’ IsClosed C β†’ C βŠ† U β†’ βˆƒ V, IsOpen V ∧ C βŠ† V ∧ closure V βŠ† UC1:Set XC2:Set XC1_closed:IsClosed C1C2_closed:IsClosed C2hC:Disjoint C1 C2V:Set XV_open:IsOpen VhV:C2 βŠ† V ∧ closure V βŠ† C1ᢜ⊒ V βŠ† closure V All goals completed! πŸ™

∎