feat: typeclass for zero-dimensional spaces

Mathlib/Topology/Algebra/ClopenNhdofOne.lean

@@ -46,9 +46,9 @@ variable {G : Type*} [Group G] [TopologicalSpace G]
 theorem exist_openNormalSubgroup_sub_open_nhds_of_one
     {U : Set G} (UOpen : IsOpen U) (einU : 1 ∈ U) :
     ∃ H : OpenNormalSubgroup G, (H : Set G) ⊆ U := by
-  rcases ((Filter.HasBasis.mem_iff' ((nhds_basis_clopen (1 : G))) U).mp <|
+  rcases ((Filter.HasBasis.mem_iff' ((hasBasis_nhds_isClopen (1 : G))) U).mp <|
     mem_nhds_iff.mpr (by use U)) with ⟨W, hW, h⟩
-  rcases IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one hW.2 hW.1 with ⟨H, hH⟩
+  rcases IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one hW.1 hW.2 with ⟨H, hH⟩
   exact ⟨H, fun _ a ↦ h (hH a)⟩
 
 open scoped Pointwise in

Mathlib/Topology/Category/LightProfinite/Basic.lean

@@ -201,7 +201,7 @@ set_option backward.isDefEq.respectTransparency false in
 theorem epi_iff_surjective {X Y : LightProfinite.{u}} (f : X ⟶ Y) :
     Epi f ↔ Function.Surjective f := by
   constructor
-  · -- Note: in mathlib3 `contrapose` saw through `Function.Surjective`.
+  · -- Porting note: in mathlib3 `contrapose` saw through `Function.Surjective`.
     dsimp [Function.Surjective]
     contrapose!
     rintro ⟨y, hy⟩ hf
@@ -213,7 +213,7 @@ theorem epi_iff_surjective {X Y : LightProfinite.{u}} (f : X ⟶ Y) :
       rintro ⟨y', hy'⟩
       exact hy y' hy'
     have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
-    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
+    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_setOf_isClopen.mem_nhds_iff.mp hUy
     classical
       let Z := of (ULift.{u} <| Fin 2)
       let g : Y ⟶ Z := CompHausLike.ofHom _

Mathlib/Topology/Category/Profinite/Basic.lean

@@ -237,7 +237,7 @@ theorem epi_iff_surjective {X Y : Profinite.{u}} (f : X ⟶ Y) : Epi f ↔ Funct
       rintro ⟨y', hy'⟩
       exact hy y' hy'
     have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
-    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
+    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_setOf_isClopen.mem_nhds_iff.mp hUy
     classical
       let Z := of (ULift.{u} <| Fin 2)
       let g : Y ⟶ Z := ofHom _

Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

@@ -48,7 +48,7 @@ theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsCl
   rotate_left
   · intro i
     change TopologicalSpace.IsTopologicalBasis {W : Set (F.obj i) | IsClopen W}
-    apply isTopologicalBasis_isClopen
+    apply isTopologicalBasis_setOf_isClopen
   · rintro i j f V (hV : IsClopen _)
     refine ⟨hV.1.preimage ?_, hV.2.preimage ?_⟩ <;> fun_prop
   -- Using this, since `U` is open, we can write `U` as a union of clopen sets all of which

Mathlib/Topology/Category/Stonean/Basic.lean

@@ -131,7 +131,7 @@ lemma epi_iff_surjective {X Y : Stonean} (f : X ⟶ Y) :
   let U := Cᶜ
   have hUy : U ∈ 𝓝 y := by
     simp only [U, C, Set.mem_range, hy, exists_false, not_false_eq_true, hC.compl_mem_nhds]
-  obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
+  obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_setOf_isClopen.mem_nhds_iff.mp hUy
   classical
   let g : Y ⟶ mkFinite (ULift (Fin 2)) := ConcreteCategory.ofHom
     ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩

Mathlib/Topology/ClopenBox.lean

@@ -82,15 +82,13 @@ instance finite_prod [Finite (Clopens X)] [Finite (Clopens Y)] :
   cases nonempty_fintype (Clopens Y)
   exact .of_surjective _ surjective_finset_sup_prod
 
-lemma countable_iff_secondCountable [T2Space X]
-    [TotallyDisconnectedSpace X] : Countable (Clopens X) ↔ SecondCountableTopology X := by
-  refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
+lemma countable_iff_secondCountable [T2Space X] [TotallyDisconnectedSpace X] :
+    Countable (Clopens X) ↔ SecondCountableTopology X := by
+  refine ⟨fun h ↦ ⟨_, ?_, isTopologicalBasis_setOf_isClopen.eq_generateFrom⟩, fun h ↦ ?_⟩
   · let f : {s : Set X | IsClopen s} → Clopens X := fun s ↦ ⟨s.1, s.2⟩
     exact Injective.of_eq_imp_le (f := f) (·.le) |>.countable
-  · apply IsTopologicalBasis.eq_generateFrom
-    exact loc_compact_Haus_tot_disc_of_zero_dim
-  · have : ∀ (s : Clopens X), ∃ (t : Finset (countableBasis X)), s.1 = (SetLike.coe t).sUnion :=
-      fun s ↦ eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _
+  · have (s : Clopens X) : ∃ t : Finset (countableBasis X), s.1 = (SetLike.coe t).sUnion :=
+      eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _
         (isBasis_countableBasis X) s.1 s.2.1.isCompact s.2.2
     let f : Clopens X → Finset (countableBasis X) := fun s ↦ (this s).choose
     have hf : f.Injective := by

Mathlib/Topology/Order.lean

@@ -285,6 +285,10 @@ theorem IndiscreteTopology.isClosed_iff [IndiscreteTopology α] (C : Set α) :
     IsClosed C ↔ C = ∅ ∨ C = Set.univ := by
   simp [← isOpen_compl_iff, IndiscreteTopology.isOpen_iff, Or.comm]
 
+theorem IndiscreteTopology.isClopen_iff [IndiscreteTopology α] (C : Set α) :
+    IsClopen C ↔ C = ∅ ∨ C = Set.univ := by
+  rw [IsClopen, IndiscreteTopology.isClosed_iff, IndiscreteTopology.isOpen_iff, and_self]
+
 theorem dense_indiscrete [IndiscreteTopology α] {s : Set α} (h : s.Nonempty) : Dense s := by
   simp [dense_iff_inter_open, IndiscreteTopology.isOpen_iff, h]
 
@@ -704,7 +708,7 @@ theorem isOpen_sup {t₁ t₂ : TopologicalSpace α} {s : Set α} :
     IsOpen[t₁ ⊔ t₂] s ↔ IsOpen[t₁] s ∧ IsOpen[t₂] s :=
   Iff.rfl
 
-
+@[simp]
 theorem IndiscreteTopology.nhds_eq [TopologicalSpace α] [IndiscreteTopology α] (a : α) :
     nhds a = ⊤ := by
   cases IndiscreteTopology.eq_top α

Mathlib/Topology/Order/WithTop.lean

@@ -257,15 +257,15 @@ def sumHomeomorph [OrderTop ι] : WithTop ι ≃ₜ ι ⊕ Unit where
 lemma tendsto_nhds_top_iff {α : Type*} {f : Filter α} (x : α → WithTop ι) :
     Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, i < x a := by
   obtain (h | h) := isEmpty_or_nonempty ι
-  · simpa using .of_forall fun _ ↦ Subsingleton.elim ..
+  · simp
   refine nhds_top_basis.tendsto_right_iff.trans ?_
   rw [← Set.forall_mem_range (p := (∀ᶠ a in f, · < x a)), WithTop.range_coe]
   simp
 
 lemma tendsto_coe_atTop [NoMaxOrder ι] :
     Tendsto ((↑) : ι → WithTop ι) atTop (𝓝 ⊤) := by
   obtain (h | h) := isEmpty_or_nonempty ι
-  · simpa using Subsingleton.elim ..
+  · simp
   rw [tendsto_nhds_top_iff]
   intro i
   filter_upwards [atTop_basis_Ioi.mem_of_mem (i := i) trivial]

Mathlib/Topology/Separation/CompletelyRegular.lean

@@ -5,12 +5,15 @@ Authors: Matias Heikkilä
 -/
 module
 
+public import Mathlib.Topology.Compactification.StoneCech
+public import Mathlib.Topology.Separation.Profinite
 public import Mathlib.Topology.UrysohnsLemma
 public import Mathlib.Topology.UnitInterval
-public import Mathlib.Topology.Compactification.StoneCech
 public import Mathlib.Topology.Order.Lattice
 public import Mathlib.Analysis.Real.Cardinality
 
+import Mathlib.Topology.Algebra.Indicator
+
 /-!
 # Completely regular topological spaces.
 
@@ -193,11 +196,23 @@ lemma completelyRegularSpace_iff_isInducing_stoneCechUnit :
   mp _ := isInducing_stoneCechUnit
   mpr hs := hs.completelyRegularSpace
 
+instance [ZeroDimensionalSpace X] : CompletelyRegularSpace X where
+  completely_regular x K hK hx := by
+    obtain ⟨s, hs, hx, hsK⟩ :=
+      isTopologicalBasis_setOf_isClopen.exists_subset_of_mem_open hx hK.isOpen_compl
+    refine ⟨(sᶜ).indicator 1, ?_, ?_, fun x hx ↦ indicator_of_mem ?_ _⟩
+    · exact hs.compl.continuous_indicator continuous_const
+    · simpa
+    · exact fun hs ↦ hsK hs hx
+
+@[deprecated inferInstance (since := "2026-03-31")]
+alias CompletelyRegularSpace.of_isTopologicalBasis_clopens :=
+  instCompletelyRegularSpaceOfZeroDimensionalSpace
+
 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 ↦ ?_)
+theorem CompletelyRegularSpace.zeroDimensionalSpace_of_cardinalMk_lt_continuum
+    [CompletelyRegularSpace X] (hX : Cardinal.mk X < continuum) : ZeroDimensionalSpace X := by
+  refine .of_isOpen_of_nhds 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
@@ -215,6 +230,10 @@ theorem CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_conti
     contrapose!; intro hxs
     simpa [hf₁ hxs] using le_one'
 
+@[deprecated (since := "2026-03-31")]
+alias CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum :=
+  CompletelyRegularSpace.zeroDimensionalSpace_of_cardinalMk_lt_continuum
+
 /-- 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
@@ -271,3 +290,12 @@ lemma t35Space_iff_isEmbedding_stoneCechUnit :
     T35Space X ↔ IsEmbedding (stoneCechUnit : X → StoneCech X) where
   mp _ := isEmbedding_stoneCechUnit
   mpr hs := hs.t35Space
+
+theorem CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum [T35Space X]
+    (h : Cardinal.mk X < .continuum) : TotallySeparatedSpace X :=
+  have := CompletelyRegularSpace.zeroDimensionalSpace_of_cardinalMk_lt_continuum h
+  inferInstance
+
+instance [Countable X] [T35Space X] : TotallySeparatedSpace X :=
+  CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum <|
+    (Cardinal.mk_le_aleph0_iff.mpr inferInstance).trans_lt Cardinal.aleph0_lt_continuum

Mathlib/Topology/Separation/DisjointCover.lean

@@ -42,7 +42,7 @@ lemma exists_finite_clopen_cover (hU : IsOpenCover U) : ∃ (n : ℕ) (V : Fin n
   -- Choose an index `r x` for each point in `X` such that `∀ x, x ∈ U (r x)`.
   choose r hr using hU.exists_mem
   -- Choose a clopen neighbourhood `V x` of each `x` contained in `U (r x)`.
-  choose V hV hVx hVU using fun x ↦ compact_exists_isClopen_in_isOpen (U _).isOpen (hr x)
+  choose V hV hVx hVU using fun x ↦ exists_isClopen_mem_of_isOpen (U _).isOpen (hr x)
   -- Apply compactness to extract a finite subset of the `V`s which covers `X`.
   obtain ⟨t, ht⟩ : ∃ t, univ ⊆ ⋃ i ∈ t, V i :=
     isCompact_univ.elim_finite_subcover V (fun x ↦ (hV x).2) (fun x _ ↦ mem_iUnion.mpr ⟨x, hVx x⟩)

Mathlib/Topology/Separation/Lemmas.lean

@@ -17,26 +17,6 @@ public import Mathlib.Topology.Separation.Profinite
 
 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