feat(topology/separation): define T₅ spaces (#16533)

I'm going to prove that any `order_topology` is a `t5_space` in a follow-up PR. This will imply that any set in an `order_topology` is a normal space.

counterexamples/sorgenfrey_line.lean

@@ -16,8 +16,9 @@ import data.set.intervals.monotone
 In this file we define `sorgenfrey_line` (notation: `ℝₗ`) to be the Sorgenfrey line. It is the real
 line with the topology space structure generated by half-open intervals `set.Ico a b`.
 
-We prove that this line is a normal space but its product with itself is not a normal space. In
-particular, this implies that the topology on `ℝₗ` is neither metrizable, nor second countable.
+We prove that this line is a completely normal Hausdorff space but its product with itself is not a
+normal space. In particular, this implies that the topology on `ℝₗ` is neither metrizable, nor
+second countable.
 
 ## Notations
 
@@ -152,30 +153,30 @@ instance : totally_disconnected_space ℝₗ :=
 
 instance : first_countable_topology ℝₗ := ⟨λ x, (nhds_basis_Ico_rat x).is_countably_generated⟩
 
-/-- Sorgenfrey line is a normal topological space. -/
-instance : normal_space ℝₗ :=
+/-- Sorgenfrey line is a completely normal Hausdorff topological space. -/
+instance : t5_space ℝₗ :=
 begin
   /- Let `s` and `t` be disjoint closed sets. For each `x ∈ s` we choose `X x` such that
   `set.Ico x (X x)` is disjoint with `t`. Similarly, for each `y ∈ t` we choose `Y y` such that
   `set.Ico y (Y y)` is disjoint with `s`. Then `⋃ x ∈ s, Ico x (X x)` and `⋃ y ∈ t, Ico y (Y y)` are
   disjoint open sets that include `s` and `t`. -/
-  refine ⟨λ s t hs ht hd, _⟩,
-  choose! X hX hXd using λ x (hx : x ∈ s), exists_Ico_disjoint_closed ht (disjoint_left.1 hd hx),
-  choose! Y hY hYd using λ y (hy : y ∈ t), exists_Ico_disjoint_closed hs (disjoint_right.1 hd hy),
-  refine ⟨⋃ x ∈ s, Ico x (X x), ⋃ y ∈ t, Ico y (Y y), is_open_bUnion $ λ _ _, is_open_Ico _ _,
-    is_open_bUnion $ λ _ _, is_open_Ico _ _, _, _, _⟩,
-  { exact λ x hx, mem_Union₂.2 ⟨x, hx, left_mem_Ico.2 $ hX x hx⟩ },
-  { exact λ y hy, mem_Union₂.2 ⟨y, hy, left_mem_Ico.2 $ hY y hy⟩ },
-  { simp only [disjoint_Union_left, disjoint_Union_right, Ico_disjoint_Ico],
-    intros y hy x hx,
-    clear hs ht hd hX hY,
-    cases le_total x y with hle hle,
-    { calc min (X x) (Y y) ≤ X x : min_le_left _ _
-      ... ≤ y : not_lt.1 (λ hyx, hXd x hx ⟨⟨hle, hyx⟩, hy⟩)
-      ... ≤ max x y : le_max_right _ _ },
-    { calc min (X x) (Y y) ≤ Y y : min_le_right _ _
-      ... ≤ x : not_lt.1 $ λ hxy, hYd y hy ⟨⟨hle, hxy⟩, hx⟩
-      ... ≤ max x y : le_max_left _ _ } }
+  refine ⟨λ s t hd₁ hd₂, _⟩,
+  choose! X hX hXd
+    using λ x (hx : x ∈ s), exists_Ico_disjoint_closed is_closed_closure (disjoint_left.1 hd₂ hx),
+  choose! Y hY hYd
+    using λ y (hy : y ∈ t), exists_Ico_disjoint_closed is_closed_closure (disjoint_right.1 hd₁ hy),
+  refine disjoint_of_disjoint_of_mem _
+    (bUnion_mem_nhds_set $ λ x hx, (is_open_Ico x (X x)).mem_nhds $ left_mem_Ico.2 (hX x hx))
+    (bUnion_mem_nhds_set $ λ y hy, (is_open_Ico y (Y y)).mem_nhds $ left_mem_Ico.2 (hY y hy)),
+  simp only [disjoint_Union_left, disjoint_Union_right, Ico_disjoint_Ico],
+  intros y hy x hx,
+  cases le_total x y with hle hle,
+  { calc min (X x) (Y y) ≤ X x : min_le_left _ _
+    ... ≤ y : not_lt.1 (λ hyx, hXd x hx ⟨⟨hle, hyx⟩, subset_closure hy⟩)
+    ... ≤ max x y : le_max_right _ _ },
+  { calc min (X x) (Y y) ≤ Y y : min_le_right _ _
+    ... ≤ x : not_lt.1 $ λ hxy, hYd y hy ⟨⟨hle, hxy⟩, subset_closure hx⟩
+    ... ≤ max x y : le_max_left _ _ }
 end
 
 lemma dense_range_coe_rat : dense_range (coe : ℚ → ℝₗ) :=

src/topology/maps.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
 import topology.order
+import topology.nhds_set
 
 /-!
 # Specific classes of maps between topological spaces
@@ -77,6 +78,10 @@ lemma inducing.nhds_eq_comap {f : α → β} (hf : inducing f) :
   ∀ (a : α), 𝓝 a = comap f (𝓝 $ f a) :=
 inducing_iff_nhds.1 hf
 
+lemma inducing.nhds_set_eq_comap {f : α → β} (hf : inducing f) (s : set α) :
+  𝓝ˢ s = comap f (𝓝ˢ (f '' s)) :=
+by simp only [nhds_set, Sup_image, comap_supr, hf.nhds_eq_comap, supr_image]
+
 lemma inducing.map_nhds_eq {f : α → β} (hf : inducing f) (a : α) :
   (𝓝 a).map f = 𝓝[range f] (f a) :=
 hf.induced.symm ▸ map_nhds_induced_eq a

src/topology/nhds_set.lean

@@ -41,6 +41,9 @@ by { rw [nhds_set, ← range_diag, ← range_comp], refl }
 lemma mem_nhds_set_iff_forall : s ∈ 𝓝ˢ t ↔ ∀ (x : α), x ∈ t → s ∈ 𝓝 x :=
 by simp_rw [nhds_set, filter.mem_Sup, ball_image_iff]
 
+lemma bUnion_mem_nhds_set {t : α → set α} (h : ∀ x ∈ s, t x ∈ 𝓝 x) : (⋃ x ∈ s, t x) ∈ 𝓝ˢ s :=
+mem_nhds_set_iff_forall.2 $ λ x hx, mem_of_superset (h x hx) (subset_Union₂ x hx)
+
 lemma subset_interior_iff_mem_nhds_set : s ⊆ interior t ↔ t ∈ 𝓝ˢ s :=
 by simp_rw [mem_nhds_set_iff_forall, subset_interior_iff_nhds]
 

src/topology/separation.lean

@@ -31,6 +31,7 @@ This file defines the predicate `separated`, and common separation axioms
 * `normal_space`: A T₄ space (sometimes referred to as normal, but authors vary on
   whether this includes T₂; `mathlib` does), is one where given two disjoint closed sets,
   we can find two open sets that separate them. In `mathlib`, T₄ implies T₃.
+* `t5_space`: A T₅ space, also known as a *completely normal Hausdorff space*
 
 ## Main results
 
@@ -105,6 +106,11 @@ def separated : set α → set α → Prop :=
   λ (s t : set α), ∃ U V : (set α), (is_open U) ∧ is_open V ∧
   (s ⊆ U) ∧ (t ⊆ V) ∧ disjoint U V
 
+lemma separated_iff_disjoint {s t : set α} :
+  separated s t ↔ disjoint (𝓝ˢ s) (𝓝ˢ t) :=
+by simp only [(has_basis_nhds_set s).disjoint_iff (has_basis_nhds_set t), separated, exists_prop,
+  ← exists_and_distrib_left, and.assoc, and.comm, and.left_comm]
+
 namespace separated
 
 open separated
@@ -142,11 +148,7 @@ lemma mono {s₁ s₂ t₁ t₂ : set α} (h : separated s₂ t₂) (hs : s₁ 
 let ⟨U, V, hU, hV, hsU, htV, hd⟩ := h in ⟨U, V, hU, hV, hs.trans hsU, ht.trans htV, hd⟩
 
 lemma union_left {a b c : set α} : separated a c → separated b c → separated (a ∪ b) c :=
-λ ⟨U, V, oU, oV, aU, bV, UV⟩ ⟨W, X, oW, oX, aW, bX, WX⟩,
-  ⟨U ∪ W, V ∩ X, is_open.union oU oW, is_open.inter oV oX,
-    union_subset_union aU aW, subset_inter bV bX, set.disjoint_union_left.mpr
-    ⟨disjoint_of_subset_right (inter_subset_left _ _) UV,
-      disjoint_of_subset_right (inter_subset_right _ _) WX⟩⟩
+by simpa only [separated_iff_disjoint, nhds_set_union, disjoint_sup_left] using and.intro
 
 lemma union_right {a b c : set α} (ab : separated a b) (ac : separated a c) :
   separated a (b ∪ c) :=
@@ -1484,6 +1486,42 @@ end
 
 end normality
 
+section completely_normal
+
+/-- A topological space `α` is a *completely normal Hausdorff space* if each subspace `s : set α` is
+a normal Hausdorff space. Equivalently, `α` is a `T₁` space and for any two sets `s`, `t` such that
+`closure s` is disjoint with `t` and `s` is disjoint with `closure t`, there exist disjoint
+neighbourhoods of `s` and `t`. -/
+class t5_space (α : Type u) [topological_space α] extends t1_space α : Prop :=
+(completely_normal : ∀ ⦃s t : set α⦄, disjoint (closure s) t → disjoint s (closure t) →
+  disjoint (𝓝ˢ s) (𝓝ˢ t))
+
+export t5_space (completely_normal)
+
+lemma embedding.t5_space [topological_space β] [t5_space β] {e : α → β} (he : embedding e) :
+  t5_space α :=
+begin
+  haveI := he.t1_space,
+  refine ⟨λ s t hd₁ hd₂, _⟩,
+  simp only [he.to_inducing.nhds_set_eq_comap],
+  refine disjoint_comap (completely_normal _ _),
+  { rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
+      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left] },
+  { rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
+      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right] }
+end
+
+/-- A subspace of a `T₅` space is a `T₅` space. -/
+instance [t5_space α] {p : α → Prop} : t5_space {x // p x} := embedding_subtype_coe.t5_space
+
+/-- A `T₅` space is a `T₄` space. -/
+@[priority 100] -- see Note [lower instance priority]
+instance t5_space.to_normal_space [t5_space α] : normal_space α :=
+⟨λ s t hs ht hd, separated_iff_disjoint.2 $
+  completely_normal (by rwa [hs.closure_eq]) (by rwa [ht.closure_eq])⟩
+
+end completely_normal
+
 /-- In a compact t2 space, the connected component of a point equals the intersection of all
 its clopen neighbourhoods. -/
 lemma connected_component_eq_Inter_clopen [t2_space α] [compact_space α] (x : α) :