feat(Topology/Separation): completely normal iff hereditarily normal (leanprover-community#32764)

Prove a space is completely normal iff it is hereditarily normal iff all open subspaces are normal.

Author: plp127

Mathlib/Topology/Separation/Regular.lean

@@ -591,6 +591,53 @@ instance ULift.instCompletelyNormalSpace [CompletelyNormalSpace X] :
     CompletelyNormalSpace (ULift X) :=
   IsEmbedding.uliftDown.completelyNormalSpace
 
+/--
+A space is completely normal iff all open subspaces are normal.
+-/
+theorem completelyNormalSpace_iff_forall_isOpen_normalSpace :
+    CompletelyNormalSpace X ↔ ∀ s : Set X, IsOpen s → NormalSpace s := by
+  refine ⟨fun _ _ _ => inferInstance, fun h => ⟨fun s t hSt hsT => ?_⟩⟩
+  let e := (closure s ∩ closure t)ᶜ
+  have he : IsOpen e := (isClosed_closure.inter isClosed_closure).isOpen_compl
+  specialize h e he
+  have hst : Disjoint (((↑) : e → X) ⁻¹' closure s) (((↑) : e → X) ⁻¹' closure t) := by
+    rw [disjoint_left]
+    intro x hxs hxt
+    exact x.2 ⟨hxs, hxt⟩
+  obtain ⟨U, V, hU, hV, hsU, htV, hUV⟩ := normal_separation
+    (isClosed_closure.preimage continuous_subtype_val)
+    (isClosed_closure.preimage continuous_subtype_val) hst
+  rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV
+  obtain ⟨U, hU, rfl⟩ := hU
+  obtain ⟨V, hV, rfl⟩ := hV
+  rw [← separatedNhds_iff_disjoint]
+  rw [Subtype.preimage_val_subset_preimage_val_iff, inter_comm e, inter_comm e] at hsU htV
+  refine ⟨U ∩ e, V ∩ e, hU.inter he, hV.inter he, ?_, ?_, ?_⟩
+  · intro x hx
+    exact hsU ⟨subset_closure hx, fun h => hsT.notMem_of_mem_left hx h.2⟩
+  · intro x hx
+    exact htV ⟨subset_closure hx, fun h => hSt.notMem_of_mem_left h.1 hx⟩
+  · rw [disjoint_left] at hUV ⊢
+    intro x hxU hxV
+    exact @hUV ⟨x, hxU.2⟩ hxU.1 hxV.1
+
+/--
+A space is completely normal iff it is hereditarily normal.
+-/
+theorem completelyNormalSpace_iff_forall_normalSpace :
+    CompletelyNormalSpace X ↔ ∀ s : Set X, NormalSpace s :=
+  ⟨fun _ _ => inferInstance, fun h =>
+    completelyNormalSpace_iff_forall_isOpen_normalSpace.2 fun s _ => h s⟩
+
+alias ⟨_, CompletelyNormalSpace.of_forall_isOpen_normalSpace⟩ :=
+  completelyNormalSpace_iff_forall_isOpen_normalSpace
+alias ⟨_, CompletelyNormalSpace.of_forall_normalSpace⟩ :=
+  completelyNormalSpace_iff_forall_normalSpace
+
+instance (priority := 100) CompletelyNormalSpace.of_regularSpace_secondCountableTopology
+    [RegularSpace X] [SecondCountableTopology X] : CompletelyNormalSpace X :=
+  .of_forall_normalSpace fun _ => .of_regularSpace_secondCountableTopology
+
 /-- A T₅ space is a completely normal T₁ space. -/
 class T5Space (X : Type u) [TopologicalSpace X] : Prop extends T1Space X, CompletelyNormalSpace X
 
@@ -616,6 +663,30 @@ instance [T5Space X] {p : X → Prop} : T5Space { x // p x } :=
 instance ULift.instT5Space [T5Space X] : T5Space (ULift X) :=
   IsEmbedding.uliftDown.t5Space
 
+/--
+A space is a `T5Space` iff all its open subspaces are `T4Space`.
+-/
+theorem t5Space_iff_forall_isOpen_t4Space :
+    T5Space X ↔ ∀ s : Set X, IsOpen s → T4Space s where
+  mp _ _ _ := inferInstance
+  mpr h :=
+    { toCompletelyNormalSpace :=
+        completelyNormalSpace_iff_forall_isOpen_normalSpace.2 fun s hs => (h s hs).toNormalSpace
+      toT1Space :=
+        have := h univ isOpen_univ
+        t1Space_of_injective_of_continuous
+          (fun _ _ => congrArg Subtype.val) (continuous_id.subtype_mk mem_univ)}
+
+/--
+A space is `T5Space` iff it is hereditarily `T4Space`.
+-/
+theorem t5Space_iff_forall_t4Space :
+    T5Space X ↔ ∀ s : Set X, T4Space s :=
+  ⟨fun _ _ => inferInstance, fun h => t5Space_iff_forall_isOpen_t4Space.2 fun s _ => h s⟩
+
+alias ⟨_, T5Space.of_forall_isOpen_t4Space⟩ := t5Space_iff_forall_isOpen_t4Space
+alias ⟨_, T5Space.of_forall_t4Space⟩ := t5Space_iff_forall_t4Space
+
 open SeparationQuotient
 
 /-- The `SeparationQuotient` of a completely normal R₀ space is a T₅ space. -/