feat: countable metric spaces are totally disconnected (leanprover-community#29211)

Prove that countable metric spaces are totally disconnected. 

This can't be placed inside `Mathlib.Topology.MetricSpace.Basic` because it causes a circular import with `Mathlib.Analysis.Real.Cardinality`. 

See also [Rat.instTotallyDisconnectedSpace](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/RatLemmas.html#Rat.instTotallyDisconnectedSpace).

There is a reference [here](https://people.math.harvard.edu/~ctm/home/text/class/harvard/131/01/html/home/course/course.pdf) for the mathematical statement and proof. 

This is upstreamed from [https://github.com/girving/ray](https://github.com/girving/ray).

Co-authored-by: Geoffrey Irving <irving@naml.us>
Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>

Author: bwangpj

Mathlib.lean

@@ -6736,6 +6736,7 @@ import Mathlib.Topology.Separation.CountableSeparatingOn
 import Mathlib.Topology.Separation.DisjointCover
 import Mathlib.Topology.Separation.GDelta
 import Mathlib.Topology.Separation.Hausdorff
+import Mathlib.Topology.Separation.Lemmas
 import Mathlib.Topology.Separation.LinearUpperLowerSetTopology
 import Mathlib.Topology.Separation.NotNormal
 import Mathlib.Topology.Separation.Profinite

Mathlib/Analysis/Real/Cardinality.lean

@@ -260,4 +260,39 @@ theorem mk_Icc_real {a b : ℝ} (h : a < b) : #(Icc a b) = 𝔠 :=
 theorem mk_Ioc_real {a b : ℝ} (h : a < b) : #(Ioc a b) = 𝔠 :=
   le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Ioc_self)
 
+@[simp]
+lemma Real.Ioo_countable_iff {x y : ℝ} :
+    (Ioo x y).Countable ↔ y ≤ x := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+  contrapose! h
+  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real h, not_le]
+  exact Cardinal.aleph0_lt_continuum
+
+@[simp]
+lemma Real.Ico_countable_iff {x y : ℝ} :
+    (Ico x y).Countable ↔ y ≤ x := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+  contrapose! h
+  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ico_real h, not_le]
+  exact Cardinal.aleph0_lt_continuum
+
+@[simp]
+lemma Real.Ioc_countable_iff {x y : ℝ} :
+    (Ioc x y).Countable ↔ y ≤ x := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+  contrapose! h
+  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real h, not_le]
+  exact Cardinal.aleph0_lt_continuum
+
+@[simp]
+lemma Real.Icc_countable_iff {x y : ℝ} :
+    (Icc x y).Countable ↔ y ≤ x := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by
+    rcases le_iff_eq_or_lt.mp h with heq | hlt
+    · simp [heq]
+    · simp [hlt]⟩
+  contrapose! h
+  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Icc_real h, not_le]
+  exact Cardinal.aleph0_lt_continuum
+
 end Cardinal

Mathlib/Topology/Separation/CompletelyRegular.lean

@@ -7,6 +7,7 @@ import Mathlib.Topology.UrysohnsLemma
 import Mathlib.Topology.UnitInterval
 import Mathlib.Topology.Compactification.StoneCech
 import Mathlib.Topology.Order.Lattice
+import Mathlib.Analysis.Real.Cardinality
 
 /-!
 # Completely regular topological spaces.
@@ -187,6 +188,28 @@ lemma completelyRegularSpace_iff_isInducing_stoneCechUnit :
   mp _ := isInducing_stoneCechUnit
   mpr hs := hs.completelyRegularSpace
 
+open TopologicalSpace Cardinal in
+theorem CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum
+    [CompletelyRegularSpace X] (hX : Cardinal.mk X < continuum) :
+    IsTopologicalBasis {s : Set X | IsClopen s} := by
+  refine isTopologicalBasis_of_isOpen_of_nhds (fun x s ↦ IsClopen.isOpen s) (fun x s hxs hs ↦ ?_)
+  choose f hf using completely_regular_isOpen x s hs hxs
+  obtain ⟨hfc, hf₀, hf₁⟩ := hf
+  let R := Set.range f
+  have hR : lift.{u, 0} (Cardinal.mk R) < lift.{0, u} continuum := by
+    simpa [R] using mk_range_le_lift.trans_lt (lift_strictMono hX)
+  rw [lift_continuum, ← lift_continuum.{u, 0}, lift_lt, ← mk_Icc_real zero_lt_one, ← unitInterval]
+    at hR
+  obtain ⟨r, hr⟩ : ∃ r : I, r ∈ Rᶜ := compl_nonempty_of_mk_lt_mk hR
+  have hr' : ∀ (x : X), f x ≠ r := by simpa [R] using hr
+  have hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r := by
+    ext; simp [le_iff_lt_or_eq, hr']
+  refine ⟨f ⁻¹' Iio r, ⟨hrclopen ▸ isClosed_Iic.preimage hfc, isOpen_Iio.preimage hfc⟩, ?_, ?_⟩
+  · simp [hf₀, hrclopen]
+  · refine preimage_subset_iff.mpr (fun x ↦ ?_)
+    contrapose!; intro hxs
+    simpa [hf₁ hxs] using le_one'
+
 /-- A T₃.₅ space is a completely regular space that is also T₀. -/
 @[mk_iff]
 class T35Space (X : Type u) [TopologicalSpace X] : Prop extends T0Space X, CompletelyRegularSpace X

Mathlib/Topology/Separation/Lemmas.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2025 Bryan Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Geoffrey Irving, Bryan Wang, Oliver Nash
+-/
+import Mathlib.Topology.GDelta.MetrizableSpace
+import Mathlib.Topology.Separation.CompletelyRegular
+import Mathlib.Topology.Separation.Profinite
+
+/-!
+# Further separation lemmas
+-/
+
+variable {X : Type*}
+
+namespace CompletelyRegularSpace
+
+variable [TopologicalSpace X] [T35Space X]
+
+theorem totallySeparatedSpace_of_cardinalMk_lt_continuum (h : Cardinal.mk X < Cardinal.continuum) :
+    TotallySeparatedSpace X :=
+  totallySeparatedSpace_of_t0_of_basis_clopen <|
+    CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum h
+
+instance [Countable X] : TotallySeparatedSpace X :=
+  totallySeparatedSpace_of_cardinalMk_lt_continuum <|
+    (Cardinal.mk_le_aleph0_iff.mpr inferInstance).trans_lt Cardinal.aleph0_lt_continuum
+
+protected lemma _root_.Set.Countable.totallySeparatedSpace {s : Set X} (h : s.Countable) :
+    TotallySeparatedSpace s :=
+  have : _root_.Countable s := h
+  inferInstanceAs (TotallySeparatedSpace s)
+
+end CompletelyRegularSpace
+
+/-- Countable subsets of metric spaces are totally disconnected. -/
+theorem Set.Countable.isTotallyDisconnected [MetricSpace X] {s : Set X} (hs : s.Countable) :
+    IsTotallyDisconnected s := by
+  rw [← totallyDisconnectedSpace_subtype_iff]
+  have : Countable s := hs
+  infer_instance

Mathlib/Topology/Separation/Profinite.lean

@@ -19,14 +19,23 @@ variable {X : Type*} {Y : Type*} [TopologicalSpace X]
 
 section Profinite
 
-/-- A T1 space with a clopen basis is totally separated. -/
-theorem totallySeparatedSpace_of_t1_of_basis_clopen [T1Space X]
+/-- A T0 space with a clopen basis is totally separated. -/
+theorem totallySeparatedSpace_of_t0_of_basis_clopen [T0Space X]
     (h : IsTopologicalBasis { s : Set X | IsClopen s }) : TotallySeparatedSpace X := by
   constructor
   rintro x - y - hxy
-  rcases h.mem_nhds_iff.mp (isOpen_ne.mem_nhds hxy) with ⟨U, hU, hxU, hyU⟩
-  exact ⟨U, Uᶜ, hU.isOpen, hU.compl.isOpen, hxU, fun h => hyU h rfl, (union_compl_self U).superset,
-    disjoint_compl_right⟩
+  choose U hU using exists_isOpen_xor'_mem hxy
+  obtain ⟨hU₀, hU₁⟩ := hU
+  rcases hU₁ with hx | hy
+  · choose V hV using h.isOpen_iff.mp hU₀ x hx.1
+    exact ⟨V, Vᶜ, hV.1.isOpen, hV.1.compl.isOpen, hV.2.1, notMem_subset hV.2.2 hx.2,
+      (union_compl_self V).superset, disjoint_compl_right⟩
+  · choose V hV using h.isOpen_iff.mp hU₀ y hy.1
+    exact ⟨Vᶜ, V, hV.1.compl.isOpen, hV.1.isOpen, notMem_subset hV.2.2 hy.2, hV.2.1,
+      (union_comm _ _ ▸ union_compl_self V).superset, disjoint_compl_left⟩
+
+@[deprecated (since := "2025-09-11")]
+alias totallySeparatedSpace_of_t1_of_basis_clopen := totallySeparatedSpace_of_t0_of_basis_clopen
 
 variable [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X]
 
@@ -109,7 +118,7 @@ theorem loc_compact_t2_tot_disc_iff_tot_sep :
     TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H := by
   constructor
   · intro h
-    exact totallySeparatedSpace_of_t1_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim
+    exact totallySeparatedSpace_of_t0_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim
   apply TotallySeparatedSpace.totallyDisconnectedSpace
 
 /-- A totally disconnected compact Hausdorff space is totally separated. -/