feat(topology/algebra/order): a linear order is T₅ (#16540)

src/data/set/intervals/ord_connected_component.lean

@@ -0,0 +1,189 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import data.set.intervals.ord_connected
+
+/-!
+# Order connected components of a set
+
+In this file we define `set.ord_connected_component s x` to be the set of `y` such that
+`set.interval x y ⊆ s` and prove some basic facts about this definition. At the moment of writing,
+this construction is used only to prove that any linear order with order topology is a T₅ space,
+so we only add API needed for this lemma.
+-/
+
+open function order_dual
+open_locale interval
+
+namespace set
+
+variables {α : Type*} [linear_order α] {s t : set α} {x y z : α}
+
+/-- Order-connected component of a point `x` in a set `s`. It is defined as the set of `y` such that
+`set.interval x y ⊆ s`. Note that it is empty if and only if `x ∉ s`. -/
+def ord_connected_component (s : set α) (x : α) : set α := {y | [x, y] ⊆ s}
+
+lemma mem_ord_connected_component : y ∈ ord_connected_component s x ↔ [x, y] ⊆ s := iff.rfl
+
+lemma dual_ord_connected_component :
+  ord_connected_component (of_dual ⁻¹' s) (to_dual x) = of_dual ⁻¹' (ord_connected_component s x) :=
+ext $ to_dual.surjective.forall.2 $ λ x,
+  by { rw [mem_ord_connected_component, dual_interval], refl }
+
+lemma ord_connected_component_subset : ord_connected_component s x ⊆ s :=
+λ y hy, hy right_mem_interval
+
+lemma subset_ord_connected_component {t} [h : ord_connected s] (hs : x ∈ s) (ht : s ⊆ t) :
+  s ⊆ ord_connected_component t x :=
+λ y hy, (h.interval_subset hs hy).trans ht
+
+@[simp] lemma self_mem_ord_connected_component : x ∈ ord_connected_component s x ↔ x ∈ s :=
+by rw [mem_ord_connected_component, interval_self, singleton_subset_iff]
+
+@[simp] lemma nonempty_ord_connected_component : (ord_connected_component s x).nonempty ↔ x ∈ s :=
+⟨λ ⟨y, hy⟩, hy $ left_mem_interval, λ h, ⟨x, self_mem_ord_connected_component.2 h⟩⟩
+
+@[simp] lemma ord_connected_component_eq_empty : ord_connected_component s x = ∅ ↔ x ∉ s :=
+by rw [← not_nonempty_iff_eq_empty, nonempty_ord_connected_component]
+
+@[simp] lemma ord_connected_component_empty : ord_connected_component ∅ x = ∅ :=
+ord_connected_component_eq_empty.2 (not_mem_empty x)
+
+@[simp] lemma ord_connected_component_univ : ord_connected_component univ x = univ :=
+by simp [ord_connected_component]
+
+lemma ord_connected_component_inter (s t : set α) (x : α) :
+  ord_connected_component (s ∩ t) x = ord_connected_component s x ∩ ord_connected_component t x :=
+by simp [ord_connected_component, set_of_and]
+
+lemma mem_ord_connected_component_comm :
+  y ∈ ord_connected_component s x ↔ x ∈ ord_connected_component s y :=
+by rw [mem_ord_connected_component, mem_ord_connected_component, interval_swap]
+
+lemma mem_ord_connected_component_trans (hxy : y ∈ ord_connected_component s x)
+  (hyz : z ∈ ord_connected_component s y) : z ∈ ord_connected_component s x :=
+calc [x, z] ⊆ [x, y] ∪ [y, z] : interval_subset_interval_union_interval
+... ⊆ s : union_subset hxy hyz
+
+lemma ord_connected_component_eq (h : [x, y] ⊆ s) :
+  ord_connected_component s x = ord_connected_component s y :=
+ext $ λ z, ⟨mem_ord_connected_component_trans (mem_ord_connected_component_comm.2 h),
+  mem_ord_connected_component_trans h⟩
+
+instance : ord_connected (ord_connected_component s x) :=
+ord_connected_of_interval_subset_left $ λ y hy z hz, (interval_subset_interval_left hz).trans hy
+
+/-- Projection from `s : set α` to `α` sending each order connected component of `s` to a single
+point of this component. -/
+noncomputable def ord_connected_proj (s : set α) : s → α :=
+λ x : s, (nonempty_ord_connected_component.2 x.prop).some
+
+lemma ord_connected_proj_mem_ord_connected_component (s : set α) (x : s) :
+  ord_connected_proj s x ∈ ord_connected_component s x :=
+nonempty.some_mem _
+
+lemma mem_ord_connected_component_ord_connected_proj (s : set α) (x : s) :
+  ↑x ∈ ord_connected_component s (ord_connected_proj s x) :=
+mem_ord_connected_component_comm.2 $ ord_connected_proj_mem_ord_connected_component s x
+
+@[simp] lemma ord_connected_component_ord_connected_proj (s : set α) (x : s) :
+  ord_connected_component s (ord_connected_proj s x) = ord_connected_component s x :=
+ord_connected_component_eq $ mem_ord_connected_component_ord_connected_proj _ _
+
+@[simp] lemma ord_connected_proj_eq {x y : s} :
+  ord_connected_proj s x = ord_connected_proj s y ↔ [(x : α), y] ⊆ s :=
+begin
+  split; intro h,
+  { rw [← mem_ord_connected_component, ← ord_connected_component_ord_connected_proj, h,
+      ord_connected_component_ord_connected_proj, self_mem_ord_connected_component],
+    exact y.2 },
+  { simp only [ord_connected_proj],
+    congr' 1,
+    exact ord_connected_component_eq h }
+end
+
+/-- A set that intersects each order connected component of a set by a single point. Defined as the
+range of `set.ord_connected_proj s`. -/
+def ord_connected_section (s : set α) : set α := range $ ord_connected_proj s
+
+lemma dual_ord_connected_section (s : set α) :
+  ord_connected_section (of_dual ⁻¹' s) = of_dual ⁻¹' (ord_connected_section s) :=
+begin
+  simp only [ord_connected_section, ord_connected_proj],
+  congr' 1 with x, simp only, congr' 1,
+  exact dual_ord_connected_component
+end
+
+lemma ord_connected_section_subset : ord_connected_section s ⊆ s :=
+range_subset_iff.2 $ λ x, ord_connected_component_subset $ nonempty.some_mem _
+
+lemma eq_of_mem_ord_connected_section_of_interval_subset (hx : x ∈ ord_connected_section s)
+  (hy : y ∈ ord_connected_section s) (h : [x, y] ⊆ s) : x = y :=
+begin
+  rcases hx with ⟨x, rfl⟩, rcases hy with ⟨y, rfl⟩,
+  exact ord_connected_proj_eq.2 (mem_ord_connected_component_trans
+    (mem_ord_connected_component_trans (ord_connected_proj_mem_ord_connected_component _ _) h)
+    (mem_ord_connected_component_ord_connected_proj _ _))
+end
+
+/-- Given two sets `s t : set α`, the set `set.order_separating_set s t` is the set of points that
+belong both to some `set.ord_connected_component tᶜ x`, `x ∈ s`, and to some
+`set.ord_connected_component sᶜ x`, `x ∈ t`. In the case of two disjoint closed sets, this is the
+union of all open intervals $(a, b)$ such that their endpoints belong to different sets. -/
+def ord_separating_set (s t : set α) : set α :=
+(⋃ x ∈ s, ord_connected_component tᶜ x) ∩ (⋃ x ∈ t, ord_connected_component sᶜ x)
+
+lemma ord_separating_set_comm (s t : set α) :
+  ord_separating_set s t = ord_separating_set t s :=
+inter_comm _ _
+
+lemma disjoint_left_ord_separating_set : disjoint s (ord_separating_set s t) :=
+disjoint.inter_right' _ $ disjoint_Union₂_right.2 $ λ x hx, disjoint_compl_right.mono_right $
+  ord_connected_component_subset
+
+lemma disjoint_right_ord_separating_set : disjoint t (ord_separating_set s t) :=
+ord_separating_set_comm t s ▸ disjoint_left_ord_separating_set
+
+lemma dual_ord_separating_set :
+  ord_separating_set (of_dual ⁻¹' s) (of_dual ⁻¹' t) = of_dual ⁻¹' (ord_separating_set s t) :=
+by simp only [ord_separating_set, mem_preimage, ← to_dual.surjective.Union_comp, of_dual_to_dual,
+  dual_ord_connected_component, ← preimage_compl, preimage_inter, preimage_Union]
+
+/-- An auxiliary neighborhood that will be used in the proof of `order_topology.t5_space`. -/
+def ord_t5_nhd (s t : set α) : set α :=
+⋃ x ∈ s, ord_connected_component (tᶜ ∩ (ord_connected_section $ ord_separating_set s t)ᶜ) x
+
+lemma disjoint_ord_t5_nhd : disjoint (ord_t5_nhd s t) (ord_t5_nhd t s) :=
+begin
+  rintro x ⟨hx₁, hx₂⟩,
+  rcases mem_Union₂.1 hx₁ with ⟨a, has, ha⟩, clear hx₁,
+  rcases mem_Union₂.1 hx₂ with ⟨b, hbt, hb⟩, clear hx₂,
+  rw [mem_ord_connected_component, subset_inter_iff] at ha hb,
+  wlog hab : a ≤ b := le_total a b using [a b s t, b a t s] tactic.skip,
+  rotate, from λ h₁ h₂ h₃ h₄, this h₂ h₁ h₄ h₃,
+  cases ha with ha ha', cases hb with hb hb',
+  have hsub : [a, b] ⊆ (ord_separating_set s t).ord_connected_sectionᶜ,
+  { rw [ord_separating_set_comm, interval_swap] at hb',
+    calc [a, b] ⊆ [a, x] ∪ [x, b] : interval_subset_interval_union_interval
+    ... ⊆ (ord_separating_set s t).ord_connected_sectionᶜ : union_subset ha' hb' },
+  clear ha' hb',
+  cases le_total x a with hxa hax,
+  { exact hb (Icc_subset_interval' ⟨hxa, hab⟩) has },
+  cases le_total b x with hbx hxb,
+  { exact ha (Icc_subset_interval ⟨hab, hbx⟩) hbt },
+  have : x ∈ ord_separating_set s t,
+  { exact ⟨mem_Union₂.2 ⟨a, has, ha⟩, mem_Union₂.2 ⟨b, hbt, hb⟩⟩ },
+  lift x to ord_separating_set s t using this,
+  suffices : ord_connected_component (ord_separating_set s t) x ⊆ [a, b],
+    from hsub (this $ ord_connected_proj_mem_ord_connected_component _ _) (mem_range_self _),
+  rintros y (hy : [↑x, y] ⊆ ord_separating_set s t),
+  rw [interval_of_le hab, mem_Icc, ← not_lt, ← not_lt],
+  exact ⟨λ hya, disjoint_left.1 disjoint_left_ord_separating_set has
+    (hy $ Icc_subset_interval' ⟨hya.le, hax⟩),
+    λ hyb, disjoint_left.1 disjoint_right_ord_separating_set hbt
+      (hy $ Icc_subset_interval ⟨hxb, hyb.le⟩)⟩
+end
+
+end set

src/topology/algebra/order/basic.lean

@@ -1120,12 +1120,6 @@ lemma dense_iff_exists_between [densely_ordered α] [nontrivial α] {s : set α}
   dense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b :=
 ⟨λ h a b hab, h.exists_between hab, dense_of_exists_between⟩
 
-@[priority 100] -- see Note [lower instance priority]
-instance order_topology.t3_space : t3_space α :=
-{ to_regular_space := regular_space.of_exists_mem_nhds_is_closed_subset $
-    λ a s hs, let ⟨b, c, ha, hmem, hs⟩ := exists_Icc_mem_subset_of_mem_nhds hs
-      in ⟨Icc b c, hmem, is_closed_Icc, hs⟩ }
-
 /-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`,
 provided `a` is neither a bottom element nor a top element. -/
 lemma mem_nhds_iff_exists_Ioo_subset' {a : α} {s : set α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :

src/topology/algebra/order/t5.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import topology.algebra.order.basic
+import data.set.intervals.ord_connected_component
+
+/-!
+# Linear order is a completely normal Hausdorff topological space
+
+In this file we prove that a linear order with order topology is a completely normal Hausdorff
+topological space.
+-/
+
+open filter set function order_dual
+open_locale topological_space filter interval
+
+variables {X : Type*} [linear_order X] [topological_space X] [order_topology X]
+  {a b c : X} {s t : set X}
+
+namespace set
+
+@[simp] lemma ord_connected_component_mem_nhds :
+  ord_connected_component s a ∈ 𝓝 a ↔ s ∈ 𝓝 a :=
+begin
+  refine ⟨λ h, mem_of_superset h ord_connected_component_subset, λ h, _⟩,
+  rcases exists_Icc_mem_subset_of_mem_nhds h with ⟨b, c, ha, ha', hs⟩,
+  exact mem_of_superset ha' (subset_ord_connected_component ha hs)
+end
+
+lemma compl_section_ord_separating_set_mem_nhds_within_Ici (hd : disjoint s (closure t))
+  (ha : a ∈ s) :
+  (ord_connected_section $ ord_separating_set s t)ᶜ ∈ 𝓝[≥] a :=
+begin
+  have hmem : tᶜ ∈ 𝓝[≥] a,
+  { refine mem_nhds_within_of_mem_nhds _,
+    rw [← mem_interior_iff_mem_nhds, interior_compl],
+    exact disjoint_left.1 hd ha },
+  rcases exists_Icc_mem_subset_of_mem_nhds_within_Ici hmem with ⟨b, hab, hmem', hsub⟩,
+  by_cases H : disjoint (Icc a b) (ord_connected_section $ ord_separating_set s t),
+  { exact mem_of_superset hmem' (disjoint_left.1 H) },
+  { simp only [set.disjoint_left, not_forall, not_not] at H,
+    rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩,
+    have hsub' : Icc a b ⊆ ord_connected_component tᶜ a,
+      from subset_ord_connected_component (left_mem_Icc.2 hab) hsub,
+    replace hac : a < c := hac.lt_of_ne (ne.symm $ ne_of_mem_of_not_mem hc $ disjoint_left.1
+      (disjoint_left_ord_separating_set.mono_right ord_connected_section_subset) ha),
+    refine mem_of_superset (Ico_mem_nhds_within_Ici (left_mem_Ico.2 hac)) (λ x hx hx', _),
+    refine hx.2.ne (eq_of_mem_ord_connected_section_of_interval_subset hx' hc _),
+    refine subset_inter (subset_Union₂_of_subset a ha _) _,
+    { exact ord_connected.interval_subset infer_instance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
+        (hsub' ⟨hac.le, hcb⟩) },
+    { rcases mem_Union₂.1 (ord_connected_section_subset hx').2 with ⟨y, hyt, hxy⟩,
+      refine subset_Union₂_of_subset y hyt (ord_connected.interval_subset infer_instance hxy _),
+      refine subset_ord_connected_component left_mem_interval hxy _,
+      suffices : c < y,
+      { rw [interval_of_ge (hx.2.trans this).le],
+        exact ⟨hx.2.le, this.le⟩ },
+      refine lt_of_not_le (λ hyc, _),
+      have hya : y < a, from not_le.1 (λ hay, hsub ⟨hay, hyc.trans hcb⟩ hyt),
+      exact hxy (Icc_subset_interval ⟨hya.le, hx.1⟩) ha } }
+end
+
+lemma compl_section_ord_separating_set_mem_nhds_within_Iic (hd : disjoint s (closure t))
+  (ha : a ∈ s) : (ord_connected_section $ ord_separating_set s t)ᶜ ∈ 𝓝[≤] a :=
+have hd' : disjoint (of_dual ⁻¹' s) (closure $ of_dual ⁻¹' t) := hd,
+have ha' : to_dual a ∈ of_dual ⁻¹' s := ha,
+by simpa only [dual_ord_separating_set, dual_ord_connected_section]
+  using compl_section_ord_separating_set_mem_nhds_within_Ici hd' ha'
+
+lemma compl_section_ord_separating_set_mem_nhds (hd : disjoint s (closure t)) (ha : a ∈ s) :
+  (ord_connected_section $ ord_separating_set s t)ᶜ ∈ 𝓝 a :=
+begin
+  rw [← nhds_left_sup_nhds_right, mem_sup],
+  exact ⟨compl_section_ord_separating_set_mem_nhds_within_Iic hd ha,
+    compl_section_ord_separating_set_mem_nhds_within_Ici hd ha⟩
+end
+
+lemma ord_t5_nhd_mem_nhds_set (hd : disjoint s (closure t)) : ord_t5_nhd s t ∈ 𝓝ˢ s :=
+bUnion_mem_nhds_set $ λ x hx, ord_connected_component_mem_nhds.2 $
+  inter_mem (by { rw [← mem_interior_iff_mem_nhds, interior_compl], exact disjoint_left.1 hd hx })
+    (compl_section_ord_separating_set_mem_nhds hd hx)
+
+end set
+
+open set
+
+/-- A linear order with order topology is a completely normal Hausdorff topological space. -/
+@[priority 100] instance order_topology.t5_space : t5_space X :=
+⟨λ s t h₁ h₂, filter.disjoint_iff.2 ⟨ord_t5_nhd s t, ord_t5_nhd_mem_nhds_set h₂, ord_t5_nhd t s,
+  ord_t5_nhd_mem_nhds_set h₁.symm, disjoint_ord_t5_nhd⟩⟩