From d9ef9ca1a36478ad62288728bfd144b0fb15b862 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sun, 19 Jul 2026 00:20:33 -0400 Subject: [PATCH 1/7] feat(Topology/Order): separability is hereditary for linearly ordered topological spaces Adds two related pieces of order-topology API: the open order-convex (`Set.OrdConnected`) sets form a topological basis of a linearly ordered topological space, and every subset of a separable such space is separable in the subspace topology. Co-Authored-By: Claude Opus 4.8 (1M context) --- Mathlib.lean | 1 + Mathlib/Topology/Order/Separable.lean | 200 ++++++++++++++++++++++++++ 2 files changed, 201 insertions(+) create mode 100644 Mathlib/Topology/Order/Separable.lean diff --git a/Mathlib.lean b/Mathlib.lean index 06874d1c0aa5ec..ad2960e5174d74 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -8120,6 +8120,7 @@ public import Mathlib.Topology.Order.ProjIcc public import Mathlib.Topology.Order.Real public import Mathlib.Topology.Order.Rolle public import Mathlib.Topology.Order.ScottTopology +public import Mathlib.Topology.Order.Separable public import Mathlib.Topology.Order.SuccPred public import Mathlib.Topology.Order.T5 public import Mathlib.Topology.Order.UpperLowerSetTopology diff --git a/Mathlib/Topology/Order/Separable.lean b/Mathlib/Topology/Order/Separable.lean new file mode 100644 index 00000000000000..f9d8d953cb4327 --- /dev/null +++ b/Mathlib/Topology/Order/Separable.lean @@ -0,0 +1,200 @@ +/- +Copyright (c) 2026 Yongxi Lin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongxi Lin +-/ +module + +public import Mathlib.Topology.Bases +public import Mathlib.Topology.Order.T5 + +/-! +# Order-convex neighbourhoods, and hereditary separability of linear orders + +A set in a preorder is *order-convex* when it contains `Set.Icc x y` for any two of its points +`x` and `y`; this is Mathlib's `Set.OrdConnected`. + +In a linearly ordered topological space the open order-convex sets form a topological basis: the +order topology is generated by the rays `Set.Iio b` and `Set.Ioi a`, and a finite intersection of +rays is `Set.Ioo a b`, a ray, or the whole space, each of which is order-convex. We obtain such a +neighbourhood as the interior of `Set.ordConnectedComponent U x`. + +The main application is that separability is hereditary for linearly ordered topological spaces: +every subset of a separable such space is separable in the subspace topology (`Set.separableSpace`). +This fails for general topological spaces, so the order is genuinely used. + +## Main results + +* `exists_isOpen_ordConnected_mem_subset`: every point of an open set has an open order-convex + neighbourhood contained in that set. +* `isTopologicalBasis_isOpen_ordConnected`: the open order-convex sets form a topological basis. +* `countable_setOf_isolated_subtype`: in a separable linearly ordered topological space, the + points of a subset that are isolated in the subspace topology form a countable set. +* `Set.separableSpace`: a separable linearly ordered topological space is hereditarily separable. + +## Implementation notes + +`Set.OrdConnected.interior` already exists, but only for spaces with `HasUpperLowerClosure` +(ordered topological groups), which does not cover a general linear order. The order-convexity of +the interior is therefore established inline in `exists_isOpen_ordConnected_mem_subset`, using +that `Set.Ioo x y` is open. +-/ + +public section + +open Filter Set TopologicalSpace +open scoped Topology + +variable {X : Type*} [TopologicalSpace X] {α : Type*} [LinearOrder α] [TopologicalSpace α] + +/-- A dense set contains every point whose singleton is open, that is, every isolated point. -/ +theorem Dense.mem_of_isOpen_singleton {s : Set X} {x : X} (hs : Dense s) + (hx : IsOpen ({x} : Set X)) : x ∈ s := by + obtain ⟨y, hys, hy⟩ := hs.exists_mem_open hx ⟨x, rfl⟩ + exact mem_singleton_iff.1 hy ▸ hys + +section OrdConnected + +variable [OrderTopology α] + +/-- Every point `x` of an open set `U` has an open order-convex neighbourhood contained in `U`. + +We take the interior of the order-connected component of `x` in `U`. Its order-convexity is where +linearity is used: if `y` and `z` lie in the interior and `y < w < z`, then `w` lies in the open +set `Set.Ioo y z`, which is contained in `Set.Icc y z` and hence in the order-convex set. -/ +theorem exists_isOpen_ordConnected_mem_subset {U : Set α} (hU : IsOpen U) {x : α} (hx : x ∈ U) : + ∃ V, IsOpen V ∧ V.OrdConnected ∧ x ∈ V ∧ V ⊆ U := by + refine ⟨interior (ordConnectedComponent U x), isOpen_interior, ⟨fun y hy z hz w hw ↦ ?_⟩, + mem_interior_iff_mem_nhds.2 (ordConnectedComponent_mem_nhds.2 (hU.mem_nhds hx)), + interior_subset.trans ordConnectedComponent_subset⟩ + rcases hw.1.eq_or_lt with rfl | hyw + · exact hy + rcases hw.2.eq_or_lt with rfl | hwz + · exact hz + exact mem_interior.2 ⟨Ioo y z, fun v hv ↦ Set.OrdConnected.out inferInstance + (interior_subset hy) (interior_subset hz) ⟨hv.1.le, hv.2.le⟩, isOpen_Ioo, hyw, hwz⟩ + +/-- The open order-convex sets form a topological basis of a linearly ordered topological +space. -/ +theorem isTopologicalBasis_isOpen_ordConnected : + IsTopologicalBasis {V : Set α | IsOpen V ∧ V.OrdConnected} := + isTopologicalBasis_of_isOpen_of_nhds (fun _ hu ↦ hu.1) fun _ _ ha hu ↦ + let ⟨V, hVo, hVc, haV, hVu⟩ := exists_isOpen_ordConnected_mem_subset hu ha + ⟨V, ⟨hVo, hVc⟩, haV, hVu⟩ + +/-- The open order-convex sets containing a point form a basis of its neighbourhood filter. -/ +theorem nhds_basis_isOpen_ordConnected (x : α) : + (𝓝 x).HasBasis (fun V : Set α ↦ (IsOpen V ∧ V.OrdConnected) ∧ x ∈ V) id := + isTopologicalBasis_isOpen_ordConnected.nhds_hasBasis + +end OrdConnected + +section Separable + +variable [OrderTopology α] + +/-- In a separable linearly ordered topological space, the points of a subset `s` that are +isolated in the subspace `↥s` form a countable set. + +Each such point `x` has an open order-convex neighbourhood `W x` meeting `s` only in `x`. The +sets `W x ∩ Ioi x` are then pairwise disjoint, as are the sets `W x ∩ Iio x`, so in a separable +space only countably many of each are nonempty; and if both are empty then `W x = {x}` is open, +so `x` belongs to any dense set. -/ +theorem countable_setOf_isolated_subtype [SeparableSpace α] (s : Set α) : + {x : s | IsOpen {x}}.Countable := by + obtain ⟨D, hDc, hDd⟩ := exists_countable_dense α + have key (x : s) (hx : IsOpen {x}) : + ∃ W, IsOpen W ∧ W.OrdConnected ∧ x.1 ∈ W ∧ W ∩ s ⊆ {x.1} := by + obtain ⟨U, hU, hUx⟩ := Topology.IsInducing.subtypeVal.isOpen_iff.1 hx + have hUs : U ∩ s ⊆ {(x : α)} := fun z hz ↦ + congrArg Subtype.val (hUx.le (show (⟨z, hz.2⟩ : s) ∈ Subtype.val ⁻¹' U from hz.1)) + obtain ⟨W, hWo, hWc, hWx, hWU⟩ := exists_isOpen_ordConnected_mem_subset hU (hUx.ge rfl) + exact ⟨W, hWo, hWc, hWx, (inter_subset_inter_left s hWU).trans hUs⟩ + choose! W hWo hWc hWx hWs using key + -- no isolated point above `x` is caught by `W x`, and none below + have hup : ∀ x : s, IsOpen {x} → ∀ y : s, (x : α) < (y : α) → + ∀ z ∈ W x, ¬ (y : α) ≤ z := fun x hx y hxy z hz hyz ↦ + hxy.ne' (hWs x hx ⟨(hWc x hx).out (hWx x hx) hz ⟨hxy.le, hyz⟩, y.2⟩) + have hdown : ∀ x : s, IsOpen {x} → ∀ y : s, (y : α) < (x : α) → + ∀ z ∈ W x, ¬ z ≤ (y : α) := fun x hx y hyx z hz hzy ↦ + hyx.ne (hWs x hx ⟨(hWc x hx).out hz (hWx x hx) ⟨hzy, hyx.le⟩, y.2⟩) + have hcr : {x : s | IsOpen {x} ∧ (W x ∩ Ioi (x : α)).Nonempty}.Countable := by + refine PairwiseDisjoint.countable_of_isOpen (s := fun x : s ↦ W x ∩ Ioi (x : α)) ?_ + (fun x hx ↦ (hWo x hx.1).inter isOpen_Ioi) fun x hx ↦ hx.2 + rintro x ⟨hx, -⟩ y ⟨hy, -⟩ hxy + refine disjoint_left.2 fun z hzx hzy ↦ ?_ + rcases lt_or_gt_of_ne (Subtype.coe_injective.ne hxy) with h | h + · exact hup x hx y h z hzx.1 hzy.2.le + · exact hup y hy x h z hzy.1 hzx.2.le + have hcl : {x : s | IsOpen {x} ∧ (W x ∩ Iio x).Nonempty}.Countable := by + refine PairwiseDisjoint.countable_of_isOpen (s := fun x : s ↦ W x ∩ Iio (x : α)) ?_ + (fun x hx ↦ (hWo x hx.1).inter isOpen_Iio) fun x hx ↦ hx.2 + rintro x ⟨hx, -⟩ y ⟨hy, -⟩ hxy + refine disjoint_left.2 fun z hzx hzy ↦ ?_ + rcases lt_or_gt_of_ne (Subtype.coe_injective.ne hxy) with h | h + · exact hdown y hy x h z hzy.1 hzx.2.le + · exact hdown x hx y h z hzx.1 hzy.2.le + -- an isolated point with nothing of `W x` on either side is isolated in `α`, hence lies in `D` + refine ((hcr.union hcl).union (hDc.preimage Subtype.val_injective)).mono fun x hx ↦ ?_ + rcases (W x ∩ Ioi x).eq_empty_or_nonempty with h₁ | h₁ + swap + · exact Or.inl (Or.inl ⟨hx, h₁⟩) + rcases (W x ∩ Iio x).eq_empty_or_nonempty with h₂ | h₂ + swap + · exact Or.inl (Or.inr ⟨hx, h₂⟩) + have hsing : W x = {x.1} := calc + _ = W x ∩ Iio x ∪ W x ∩ {x.1} ∪ W x ∩ Ioi x := by grind + _ = {x.1} := by grind + exact Or.inr (hDd.mem_of_isOpen_singleton (hsing ▸ hWo x hx)) + +/-- A separable linearly ordered topological space is hereditarily separable: every subset, +equipped with the subspace topology, is a separable space. -/ +instance Set.separableSpace [SeparableSpace α] (s : Set α) : SeparableSpace s := by + obtain ⟨D, hc, hd⟩ := exists_countable_dense α + -- a point of `s` strictly between `p` and `q`, whenever there is one + have hchoice (p q) : ∃ z : α, (s ∩ Ioo p q).Nonempty → z ∈ s ∩ Ioo p q := by + by_cases h : (s ∩ Ioo p q).Nonempty + · exact ⟨h.choose, fun _ ↦ h.choose_spec⟩ + · exact ⟨p, fun h' ↦ absurd h' h⟩ + choose a ha using hchoice + refine ⟨⟨{x : s | IsOpen {x}} ∪ Subtype.val ⁻¹' image2 a D D, + (countable_setOf_isolated_subtype s).union + ((hc.image2 hc a).preimage Subtype.val_injective), ?_⟩⟩ + refine dense_iff_inter_open.2 fun O hO ⟨x, hxO⟩ ↦ ?_ + by_cases hxiso : IsOpen {x} + · exact ⟨x, hxO, Or.inl hxiso⟩ + obtain ⟨U, hU, hUO⟩ := Topology.IsInducing.subtypeVal.isOpen_iff.1 hO + obtain ⟨W, hWo, hWc, hWx, hWU⟩ := exists_isOpen_ordConnected_mem_subset hU (hUO.ge hxO) + -- as `x` is not isolated in `↥s`, every open set containing it meets `s` in a different point + have hnot (G : Set α) (hG : IsOpen G) (hxG : x.1 ∈ G) : ∃ y ∈ s, y ∈ G ∧ y ≠ x := by + by_contra! hcon + suffices hGx : Subtype.val ⁻¹' G = {x} from hxiso (hGx ▸ hG.preimage continuous_subtype_val) + grind + -- a point `b` of `s` in `W` with points of `W` strictly on either side of it + obtain ⟨b, hbs, hlo, hhi⟩ : ∃ b ∈ s, (W ∩ Iio b).Nonempty ∧ (W ∩ Ioi b).Nonempty := by + obtain ⟨y, hys, hyW, hyx⟩ := hnot W hWo hWx + rcases hyx.lt_or_gt with hy | hy + · obtain ⟨z, hzs, hzW, hzx⟩ := hnot (W ∩ Ioi y) (hWo.inter isOpen_Ioi) ⟨hWx, hy⟩ + rcases hzx.lt_or_gt with hz | hz + · exact ⟨z, hzs, ⟨y, hyW, hzW.2⟩, ⟨x, hWx, hz⟩⟩ + · exact ⟨x, x.2, ⟨y, hyW, hy⟩, ⟨z, hzW.1, hz⟩⟩ + · obtain ⟨z, hzs, hzW, hzx⟩ := hnot (W ∩ Iio y) (hWo.inter isOpen_Iio) ⟨hWx, hy⟩ + rcases hzx.lt_or_gt with hz | hz + · exact ⟨x, x.2, ⟨z, hzW.1, hz⟩, ⟨y, hyW, hy⟩⟩ + · exact ⟨z, hzs, ⟨x, hWx, hz⟩, ⟨y, hyW, hzW.2⟩⟩ + obtain ⟨p, hpD, hpW⟩ := hd.exists_mem_open (hWo.inter isOpen_Iio) hlo + obtain ⟨q, hqD, hqW⟩ := hd.exists_mem_open (hWo.inter isOpen_Ioi) hhi + obtain ⟨hasq, hapq⟩ := ha p q ⟨b, hbs, hpW.2, hqW.2⟩ + exact ⟨⟨a p q, hasq⟩, + hUO.le (hWU (hWc.out hpW.1 hqW.1 (Ioo_subset_Icc_self hapq))), + Or.inr ⟨p, hpD, q, hqD, rfl⟩⟩ + +end Separable + +/-- A point of a subset `s` is isolated on the right in the subspace `↥s` exactly when it is +isolated on the right within `s`. -/ +theorem nhdsGT_subtype_eq_bot_iff {s : Set α} {x : s} : + 𝓝[>] x = ⊥ ↔ 𝓝[s ∩ Ioi (x : α)] (x : α) = ⊥ := by + have : ((↑) : s → α) ⁻¹' Ioi (x : α) = Ioi x := rfl + rw [← this, nhdsWithin_subtype_eq_bot_iff, nhdsWithin, inf_assoc, inf_principal, inter_comm, + ← nhdsWithin] From 3f8d5a81b612440598c34a1cfcabc96fc9a3f5a1 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sun, 19 Jul 2026 05:14:14 -0400 Subject: [PATCH 2/7] chore(Topology/Closure): move Dense.mem_of_isOpen_singleton from Order/Separable It is a general fact about dense sets with no order hypotheses, so it belongs next to Dense.exists_mem_open, which its proof uses. Also tidy the module docstring of Topology/Order/Separable and switch to "order connected" terminology. Co-Authored-By: Claude Opus 4.8 (1M context) --- Mathlib/Topology/Closure.lean | 5 +++ Mathlib/Topology/Order/Separable.lean | 62 ++++++--------------------- 2 files changed, 17 insertions(+), 50 deletions(-) diff --git a/Mathlib/Topology/Closure.lean b/Mathlib/Topology/Closure.lean index 1c1594198d825f..a3528028748492 100644 --- a/Mathlib/Topology/Closure.lean +++ b/Mathlib/Topology/Closure.lean @@ -421,6 +421,11 @@ theorem Dense.exists_mem_open (hs : Dense s) {U : Set X} (ho : IsOpen U) let ⟨x, hx⟩ := hs.inter_open_nonempty U ho hne ⟨x, hx.2, hx.1⟩ +/-- A dense set contains every point whose singleton is open, that is, every isolated point. -/ +theorem Dense.mem_of_isOpen_singleton (hs : Dense s) (hx : IsOpen {x}) : x ∈ s := by + obtain ⟨y, hys, hy⟩ := hs.exists_mem_open hx ⟨x, rfl⟩ + exact mem_singleton_iff.1 hy ▸ hys + theorem Dense.nonempty_iff (hs : Dense s) : s.Nonempty ↔ Nonempty X := ⟨fun ⟨x, _⟩ => ⟨x⟩, fun ⟨x⟩ => let ⟨y, hy⟩ := hs.inter_open_nonempty _ isOpen_univ ⟨x, trivial⟩ diff --git a/Mathlib/Topology/Order/Separable.lean b/Mathlib/Topology/Order/Separable.lean index f9d8d953cb4327..7597c849ce15ff 100644 --- a/Mathlib/Topology/Order/Separable.lean +++ b/Mathlib/Topology/Order/Separable.lean @@ -5,39 +5,22 @@ Authors: Yongxi Lin -/ module -public import Mathlib.Topology.Bases public import Mathlib.Topology.Order.T5 /-! -# Order-convex neighbourhoods, and hereditary separability of linear orders +# Hereditary separability of linear orders -A set in a preorder is *order-convex* when it contains `Set.Icc x y` for any two of its points -`x` and `y`; this is Mathlib's `Set.OrdConnected`. - -In a linearly ordered topological space the open order-convex sets form a topological basis: the -order topology is generated by the rays `Set.Iio b` and `Set.Ioi a`, and a finite intersection of -rays is `Set.Ioo a b`, a ray, or the whole space, each of which is order-convex. We obtain such a -neighbourhood as the interior of `Set.ordConnectedComponent U x`. - -The main application is that separability is hereditary for linearly ordered topological spaces: -every subset of a separable such space is separable in the subspace topology (`Set.separableSpace`). -This fails for general topological spaces, so the order is genuinely used. +In this file we prove some results about a separable linearly ordered topological space. ## Main results -* `exists_isOpen_ordConnected_mem_subset`: every point of an open set has an open order-convex +* `exists_isOpen_ordConnected_mem_subset`: every point of an open set has an open order connected neighbourhood contained in that set. -* `isTopologicalBasis_isOpen_ordConnected`: the open order-convex sets form a topological basis. +* `isTopologicalBasis_isOpen_ordConnected`: the open order connected sets form a topological basis. * `countable_setOf_isolated_subtype`: in a separable linearly ordered topological space, the points of a subset that are isolated in the subspace topology form a countable set. * `Set.separableSpace`: a separable linearly ordered topological space is hereditarily separable. -## Implementation notes - -`Set.OrdConnected.interior` already exists, but only for spaces with `HasUpperLowerClosure` -(ordered topological groups), which does not cover a general linear order. The order-convexity of -the interior is therefore established inline in `exists_isOpen_ordConnected_mem_subset`, using -that `Set.Ioo x y` is open. -/ public section @@ -45,23 +28,12 @@ public section open Filter Set TopologicalSpace open scoped Topology -variable {X : Type*} [TopologicalSpace X] {α : Type*} [LinearOrder α] [TopologicalSpace α] - -/-- A dense set contains every point whose singleton is open, that is, every isolated point. -/ -theorem Dense.mem_of_isOpen_singleton {s : Set X} {x : X} (hs : Dense s) - (hx : IsOpen ({x} : Set X)) : x ∈ s := by - obtain ⟨y, hys, hy⟩ := hs.exists_mem_open hx ⟨x, rfl⟩ - exact mem_singleton_iff.1 hy ▸ hys +variable {α : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] section OrdConnected -variable [OrderTopology α] - -/-- Every point `x` of an open set `U` has an open order-convex neighbourhood contained in `U`. - -We take the interior of the order-connected component of `x` in `U`. Its order-convexity is where -linearity is used: if `y` and `z` lie in the interior and `y < w < z`, then `w` lies in the open -set `Set.Ioo y z`, which is contained in `Set.Icc y z` and hence in the order-convex set. -/ +/-- Every point `x` of an open set `U` has an open order connected neighbourhood contained in `U`. +-/ theorem exists_isOpen_ordConnected_mem_subset {U : Set α} (hU : IsOpen U) {x : α} (hx : x ∈ U) : ∃ V, IsOpen V ∧ V.OrdConnected ∧ x ∈ V ∧ V ⊆ U := by refine ⟨interior (ordConnectedComponent U x), isOpen_interior, ⟨fun y hy z hz w hw ↦ ?_⟩, @@ -71,10 +43,10 @@ theorem exists_isOpen_ordConnected_mem_subset {U : Set α} (hU : IsOpen U) {x : · exact hy rcases hw.2.eq_or_lt with rfl | hwz · exact hz - exact mem_interior.2 ⟨Ioo y z, fun v hv ↦ Set.OrdConnected.out inferInstance + exact mem_interior.2 ⟨Ioo y z, fun v hv ↦ OrdConnected.out inferInstance (interior_subset hy) (interior_subset hz) ⟨hv.1.le, hv.2.le⟩, isOpen_Ioo, hyw, hwz⟩ -/-- The open order-convex sets form a topological basis of a linearly ordered topological +/-- The open order connected sets form a topological basis of a linearly ordered topological space. -/ theorem isTopologicalBasis_isOpen_ordConnected : IsTopologicalBasis {V : Set α | IsOpen V ∧ V.OrdConnected} := @@ -82,7 +54,7 @@ theorem isTopologicalBasis_isOpen_ordConnected : let ⟨V, hVo, hVc, haV, hVu⟩ := exists_isOpen_ordConnected_mem_subset hu ha ⟨V, ⟨hVo, hVc⟩, haV, hVu⟩ -/-- The open order-convex sets containing a point form a basis of its neighbourhood filter. -/ +/-- The open order connected sets containing a point form a basis of its neighbourhood filter. -/ theorem nhds_basis_isOpen_ordConnected (x : α) : (𝓝 x).HasBasis (fun V : Set α ↦ (IsOpen V ∧ V.OrdConnected) ∧ x ∈ V) id := isTopologicalBasis_isOpen_ordConnected.nhds_hasBasis @@ -91,12 +63,10 @@ end OrdConnected section Separable -variable [OrderTopology α] - /-- In a separable linearly ordered topological space, the points of a subset `s` that are isolated in the subspace `↥s` form a countable set. -Each such point `x` has an open order-convex neighbourhood `W x` meeting `s` only in `x`. The +Each such point `x` has an open order connected neighbourhood `W x` meeting `s` only in `x`. The sets `W x ∩ Ioi x` are then pairwise disjoint, as are the sets `W x ∩ Iio x`, so in a separable space only countably many of each are nonempty; and if both are empty then `W x = {x}` is open, so `x` belongs to any dense set. -/ @@ -165,7 +135,7 @@ instance Set.separableSpace [SeparableSpace α] (s : Set α) : SeparableSpace s · exact ⟨x, hxO, Or.inl hxiso⟩ obtain ⟨U, hU, hUO⟩ := Topology.IsInducing.subtypeVal.isOpen_iff.1 hO obtain ⟨W, hWo, hWc, hWx, hWU⟩ := exists_isOpen_ordConnected_mem_subset hU (hUO.ge hxO) - -- as `x` is not isolated in `↥s`, every open set containing it meets `s` in a different point + -- as `x` is not isolated in `s`, every open set containing it meets `s` in a different point have hnot (G : Set α) (hG : IsOpen G) (hxG : x.1 ∈ G) : ∃ y ∈ s, y ∈ G ∧ y ≠ x := by by_contra! hcon suffices hGx : Subtype.val ⁻¹' G = {x} from hxiso (hGx ▸ hG.preimage continuous_subtype_val) @@ -190,11 +160,3 @@ instance Set.separableSpace [SeparableSpace α] (s : Set α) : SeparableSpace s Or.inr ⟨p, hpD, q, hqD, rfl⟩⟩ end Separable - -/-- A point of a subset `s` is isolated on the right in the subspace `↥s` exactly when it is -isolated on the right within `s`. -/ -theorem nhdsGT_subtype_eq_bot_iff {s : Set α} {x : s} : - 𝓝[>] x = ⊥ ↔ 𝓝[s ∩ Ioi (x : α)] (x : α) = ⊥ := by - have : ((↑) : s → α) ⁻¹' Ioi (x : α) = Ioi x := rfl - rw [← this, nhdsWithin_subtype_eq_bot_iff, nhdsWithin, inf_assoc, inf_principal, inter_comm, - ← nhdsWithin] From a3603a88f42ef4c96231ad1217762d5302e663bc Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sun, 19 Jul 2026 05:28:13 -0400 Subject: [PATCH 3/7] change docstring --- Mathlib/Topology/Closure.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Closure.lean b/Mathlib/Topology/Closure.lean index a3528028748492..072a08f34e7b34 100644 --- a/Mathlib/Topology/Closure.lean +++ b/Mathlib/Topology/Closure.lean @@ -421,7 +421,7 @@ theorem Dense.exists_mem_open (hs : Dense s) {U : Set X} (ho : IsOpen U) let ⟨x, hx⟩ := hs.inter_open_nonempty U ho hne ⟨x, hx.2, hx.1⟩ -/-- A dense set contains every point whose singleton is open, that is, every isolated point. -/ +/-- A dense set contains every isolated point. -/ theorem Dense.mem_of_isOpen_singleton (hs : Dense s) (hx : IsOpen {x}) : x ∈ s := by obtain ⟨y, hys, hy⟩ := hs.exists_mem_open hx ⟨x, rfl⟩ exact mem_singleton_iff.1 hy ▸ hys From 04ae1a39d8e972b4e1a94cedc0986b5c092f77ca Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Thu, 23 Jul 2026 01:06:46 -0400 Subject: [PATCH 4/7] golf separability proofs --- Mathlib/Topology/Order/Separable.lean | 117 +++++++++++--------------- 1 file changed, 49 insertions(+), 68 deletions(-) diff --git a/Mathlib/Topology/Order/Separable.lean b/Mathlib/Topology/Order/Separable.lean index 7597c849ce15ff..a87614e67b0b4a 100644 --- a/Mathlib/Topology/Order/Separable.lean +++ b/Mathlib/Topology/Order/Separable.lean @@ -63,65 +63,54 @@ end OrdConnected section Separable -/-- In a separable linearly ordered topological space, the points of a subset `s` that are -isolated in the subspace `↥s` form a countable set. +private lemma countable_isolated_inter_Ioi_aux [SeparableSpace α] {s : Set α} {W : s → Set α} + (hWo : ∀ x, IsOpen {x} → IsOpen (W x)) (hWc : ∀ x, IsOpen {x} → (W x).OrdConnected) + (hWx : ∀ x, IsOpen {x} → {x.1} = W x ∩ s) : + {x : s | IsOpen {x} ∧ (W x ∩ Ioi x).Nonempty}.Countable := by + refine PairwiseDisjoint.countable_of_isOpen ?_ ?_ fun _ hx ↦ hx.2 + · rintro x ⟨hx, -⟩ y ⟨hy, -⟩ hxy + refine disjoint_left.2 fun z hzx hzy ↦ ?_ + rcases lt_or_gt_of_ne (Subtype.coe_injective.ne hxy) with h | h + · exact h.ne' ((hWx x hx).ge + ⟨(hWc x hx).out ((hWx x hx).le rfl).1 hzx.1 ⟨h.le, hzy.2.le⟩, y.2⟩) + · exact h.ne' ((hWx y hy).ge + ⟨(hWc y hy).out ((hWx y hy).le rfl).1 hzy.1 ⟨h.le, hzx.2.le⟩, x.2⟩) + · exact fun x hx ↦ (hWo x hx.1).inter isOpen_Ioi -Each such point `x` has an open order connected neighbourhood `W x` meeting `s` only in `x`. The -sets `W x ∩ Ioi x` are then pairwise disjoint, as are the sets `W x ∩ Iio x`, so in a separable -space only countably many of each are nonempty; and if both are empty then `W x = {x}` is open, -so `x` belongs to any dense set. -/ +/-- In a separable linearly ordered topological space, the points of a subset `s` that are +isolated in the subspace `s` form a countable set. -/ theorem countable_setOf_isolated_subtype [SeparableSpace α] (s : Set α) : {x : s | IsOpen {x}}.Countable := by obtain ⟨D, hDc, hDd⟩ := exists_countable_dense α - have key (x : s) (hx : IsOpen {x}) : - ∃ W, IsOpen W ∧ W.OrdConnected ∧ x.1 ∈ W ∧ W ∩ s ⊆ {x.1} := by + -- Each such point `x` has an open order connected neighbourhood `W x` meeting `s` only in `x`. + have key (x : s) (hx : IsOpen {x}) : ∃ W, IsOpen W ∧ W.OrdConnected ∧ {x.1} = W ∩ s := by obtain ⟨U, hU, hUx⟩ := Topology.IsInducing.subtypeVal.isOpen_iff.1 hx - have hUs : U ∩ s ⊆ {(x : α)} := fun z hz ↦ - congrArg Subtype.val (hUx.le (show (⟨z, hz.2⟩ : s) ∈ Subtype.val ⁻¹' U from hz.1)) - obtain ⟨W, hWo, hWc, hWx, hWU⟩ := exists_isOpen_ordConnected_mem_subset hU (hUx.ge rfl) - exact ⟨W, hWo, hWc, hWx, (inter_subset_inter_left s hWU).trans hUs⟩ - choose! W hWo hWc hWx hWs using key - -- no isolated point above `x` is caught by `W x`, and none below - have hup : ∀ x : s, IsOpen {x} → ∀ y : s, (x : α) < (y : α) → - ∀ z ∈ W x, ¬ (y : α) ≤ z := fun x hx y hxy z hz hyz ↦ - hxy.ne' (hWs x hx ⟨(hWc x hx).out (hWx x hx) hz ⟨hxy.le, hyz⟩, y.2⟩) - have hdown : ∀ x : s, IsOpen {x} → ∀ y : s, (y : α) < (x : α) → - ∀ z ∈ W x, ¬ z ≤ (y : α) := fun x hx y hyx z hz hzy ↦ - hyx.ne (hWs x hx ⟨(hWc x hx).out hz (hWx x hx) ⟨hzy, hyx.le⟩, y.2⟩) - have hcr : {x : s | IsOpen {x} ∧ (W x ∩ Ioi (x : α)).Nonempty}.Countable := by - refine PairwiseDisjoint.countable_of_isOpen (s := fun x : s ↦ W x ∩ Ioi (x : α)) ?_ - (fun x hx ↦ (hWo x hx.1).inter isOpen_Ioi) fun x hx ↦ hx.2 - rintro x ⟨hx, -⟩ y ⟨hy, -⟩ hxy - refine disjoint_left.2 fun z hzx hzy ↦ ?_ - rcases lt_or_gt_of_ne (Subtype.coe_injective.ne hxy) with h | h - · exact hup x hx y h z hzx.1 hzy.2.le - · exact hup y hy x h z hzy.1 hzx.2.le - have hcl : {x : s | IsOpen {x} ∧ (W x ∩ Iio x).Nonempty}.Countable := by - refine PairwiseDisjoint.countable_of_isOpen (s := fun x : s ↦ W x ∩ Iio (x : α)) ?_ - (fun x hx ↦ (hWo x hx.1).inter isOpen_Iio) fun x hx ↦ hx.2 - rintro x ⟨hx, -⟩ y ⟨hy, -⟩ hxy - refine disjoint_left.2 fun z hzx hzy ↦ ?_ - rcases lt_or_gt_of_ne (Subtype.coe_injective.ne hxy) with h | h - · exact hdown y hy x h z hzy.1 hzx.2.le - · exact hdown x hx y h z hzx.1 hzy.2.le - -- an isolated point with nothing of `W x` on either side is isolated in `α`, hence lies in `D` + obtain ⟨W, hWo, hWc, hxW, hWU⟩ := exists_isOpen_ordConnected_mem_subset hU (hUx.ge rfl) + refine ⟨W, hWo, hWc, Subset.antisymm (fun _ h ↦ h ▸ ⟨hxW, x.2⟩) fun y hy ↦ ?_⟩ + exact congrArg Subtype.val <| + hUx.le (show (⟨y, hy.2⟩ : s) ∈ Subtype.val ⁻¹' U from hWU hy.1) + choose! W hWo hWc hWx using key + -- The sets `W x ∩ Ioi x` are then pairwise disjoint, as are the sets `W x ∩ Iio x`. + have hcr : {x : s | IsOpen {x} ∧ (W x ∩ Ioi x).Nonempty}.Countable := + countable_isolated_inter_Ioi_aux hWo hWc hWx + have hcl : {x : s | IsOpen {x} ∧ (W x ∩ Iio x).Nonempty}.Countable := + countable_isolated_inter_Ioi_aux (α := αᵒᵈ) hWo (fun x hx ↦ (hWc x hx).dual) hWx + -- An isolated point with nothing of `W x` on either side is isolated in `α`, hence lies in `D`. refine ((hcr.union hcl).union (hDc.preimage Subtype.val_injective)).mono fun x hx ↦ ?_ rcases (W x ∩ Ioi x).eq_empty_or_nonempty with h₁ | h₁ - swap - · exact Or.inl (Or.inl ⟨hx, h₁⟩) - rcases (W x ∩ Iio x).eq_empty_or_nonempty with h₂ | h₂ - swap - · exact Or.inl (Or.inr ⟨hx, h₂⟩) - have hsing : W x = {x.1} := calc - _ = W x ∩ Iio x ∪ W x ∩ {x.1} ∪ W x ∩ Ioi x := by grind - _ = {x.1} := by grind - exact Or.inr (hDd.mem_of_isOpen_singleton (hsing ▸ hWo x hx)) + · rcases (W x ∩ Iio x).eq_empty_or_nonempty with h₂ | h₂ + · have hsing : W x = {x.1} := calc + _ = W x ∩ Iio x ∪ W x ∩ {x.1} ∪ W x ∩ Ioi x := by grind + _ = {x.1} := by grind + exact .inr (hDd.mem_of_isOpen_singleton (hsing ▸ hWo x hx)) + · exact .inl (.inr ⟨hx, h₂⟩) + · exact .inl (.inl ⟨hx, h₁⟩) /-- A separable linearly ordered topological space is hereditarily separable: every subset, equipped with the subspace topology, is a separable space. -/ instance Set.separableSpace [SeparableSpace α] (s : Set α) : SeparableSpace s := by obtain ⟨D, hc, hd⟩ := exists_countable_dense α - -- a point of `s` strictly between `p` and `q`, whenever there is one + -- A point of `s` strictly between `p` and `q`, whenever there is one. have hchoice (p q) : ∃ z : α, (s ∩ Ioo p q).Nonempty → z ∈ s ∩ Ioo p q := by by_cases h : (s ∩ Ioo p q).Nonempty · exact ⟨h.choose, fun _ ↦ h.choose_spec⟩ @@ -132,31 +121,23 @@ instance Set.separableSpace [SeparableSpace α] (s : Set α) : SeparableSpace s ((hc.image2 hc a).preimage Subtype.val_injective), ?_⟩⟩ refine dense_iff_inter_open.2 fun O hO ⟨x, hxO⟩ ↦ ?_ by_cases hxiso : IsOpen {x} - · exact ⟨x, hxO, Or.inl hxiso⟩ + · exact ⟨x, hxO, .inl hxiso⟩ obtain ⟨U, hU, hUO⟩ := Topology.IsInducing.subtypeVal.isOpen_iff.1 hO obtain ⟨W, hWo, hWc, hWx, hWU⟩ := exists_isOpen_ordConnected_mem_subset hU (hUO.ge hxO) - -- as `x` is not isolated in `s`, every open set containing it meets `s` in a different point - have hnot (G : Set α) (hG : IsOpen G) (hxG : x.1 ∈ G) : ∃ y ∈ s, y ∈ G ∧ y ≠ x := by - by_contra! hcon - suffices hGx : Subtype.val ⁻¹' G = {x} from hxiso (hGx ▸ hG.preimage continuous_subtype_val) - grind - -- a point `b` of `s` in `W` with points of `W` strictly on either side of it - obtain ⟨b, hbs, hlo, hhi⟩ : ∃ b ∈ s, (W ∩ Iio b).Nonempty ∧ (W ∩ Ioi b).Nonempty := by - obtain ⟨y, hys, hyW, hyx⟩ := hnot W hWo hWx - rcases hyx.lt_or_gt with hy | hy - · obtain ⟨z, hzs, hzW, hzx⟩ := hnot (W ∩ Ioi y) (hWo.inter isOpen_Ioi) ⟨hWx, hy⟩ - rcases hzx.lt_or_gt with hz | hz - · exact ⟨z, hzs, ⟨y, hyW, hzW.2⟩, ⟨x, hWx, hz⟩⟩ - · exact ⟨x, x.2, ⟨y, hyW, hy⟩, ⟨z, hzW.1, hz⟩⟩ - · obtain ⟨z, hzs, hzW, hzx⟩ := hnot (W ∩ Iio y) (hWo.inter isOpen_Iio) ⟨hWx, hy⟩ - rcases hzx.lt_or_gt with hz | hz - · exact ⟨x, x.2, ⟨z, hzW.1, hz⟩, ⟨y, hyW, hy⟩⟩ - · exact ⟨z, hzs, ⟨x, hWx, hz⟩, ⟨y, hyW, hzW.2⟩⟩ + -- A point `b` of `s` in `W` with points of `W` strictly on either side of it. + obtain ⟨b, hbs, hlo, hhi⟩ : + ∃ b ∈ s, (W ∩ Iio b).Nonempty ∧ (W ∩ Ioi b).Nonempty := by + rw [isOpen_singleton_iff_punctured_nhds] at hxiso + let : NeBot (𝓝[≠] x) := ⟨hxiso⟩ + have hWinf : (Subtype.val ⁻¹' W).Infinite := + infinite_of_mem_nhds x ((hWo.preimage continuous_subtype_val).mem_nhds hWx) + by_contra! h + exact hWinf (finite_of_forall_not_lt_lt fun a ha b hb c hc hab hbc ↦ + (congrArg ((c : α) ∈ ·) (h b b.2 ⟨a, ha, hab⟩)).mp ⟨hc, hbc⟩) obtain ⟨p, hpD, hpW⟩ := hd.exists_mem_open (hWo.inter isOpen_Iio) hlo obtain ⟨q, hqD, hqW⟩ := hd.exists_mem_open (hWo.inter isOpen_Ioi) hhi obtain ⟨hasq, hapq⟩ := ha p q ⟨b, hbs, hpW.2, hqW.2⟩ - exact ⟨⟨a p q, hasq⟩, - hUO.le (hWU (hWc.out hpW.1 hqW.1 (Ioo_subset_Icc_self hapq))), - Or.inr ⟨p, hpD, q, hqD, rfl⟩⟩ + exact ⟨⟨a p q, hasq⟩, hUO.le (hWU (hWc.out hpW.1 hqW.1 (Ioo_subset_Icc_self hapq))), + .inr ⟨p, hpD, q, hqD, rfl⟩⟩ end Separable From c854586e5eeaca3b359ca37b9908077ff6edc827 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Wed, 29 Jul 2026 19:47:51 -0700 Subject: [PATCH 5/7] docs(Topology): note GO-space generalization --- Mathlib/Topology/Order/Separable.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Topology/Order/Separable.lean b/Mathlib/Topology/Order/Separable.lean index a87614e67b0b4a..da721483cbbc9b 100644 --- a/Mathlib/Topology/Order/Separable.lean +++ b/Mathlib/Topology/Order/Separable.lean @@ -21,6 +21,8 @@ In this file we prove some results about a separable linearly ordered topologica points of a subset that are isolated in the subspace topology form a countable set. * `Set.separableSpace`: a separable linearly ordered topological space is hereditarily separable. +TODO: Generalize the hereditary separability result to separable GO-spaces. + -/ public section From fefc8192e55aae13a6446a244e45bd000d1e3dc0 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Wed, 29 Jul 2026 19:49:35 -0700 Subject: [PATCH 6/7] docs(Topology): clarify GO-space TODO --- Mathlib/Topology/Order/Separable.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/Order/Separable.lean b/Mathlib/Topology/Order/Separable.lean index da721483cbbc9b..831544d13783f0 100644 --- a/Mathlib/Topology/Order/Separable.lean +++ b/Mathlib/Topology/Order/Separable.lean @@ -21,7 +21,8 @@ In this file we prove some results about a separable linearly ordered topologica points of a subset that are isolated in the subspace topology form a countable set. * `Set.separableSpace`: a separable linearly ordered topological space is hereditarily separable. -TODO: Generalize the hereditary separability result to separable GO-spaces. +##TODO: +Define the class of GO-spaces and generalize the hereditary separability result. -/ From 73788e18dacc89dfc41bc4de9f3bc547f05537ea Mon Sep 17 00:00:00 2001 From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com> Date: Wed, 29 Jul 2026 19:50:57 -0700 Subject: [PATCH 7/7] Update Separable.lean --- Mathlib/Topology/Order/Separable.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/Order/Separable.lean b/Mathlib/Topology/Order/Separable.lean index 831544d13783f0..eed42324787583 100644 --- a/Mathlib/Topology/Order/Separable.lean +++ b/Mathlib/Topology/Order/Separable.lean @@ -21,7 +21,8 @@ In this file we prove some results about a separable linearly ordered topologica points of a subset that are isolated in the subspace topology form a countable set. * `Set.separableSpace`: a separable linearly ordered topological space is hereditarily separable. -##TODO: +## TODO + Define the class of GO-spaces and generalize the hereditary separability result. -/