feat(Topology/CWComplex/Classical): discrete spaces are CW complexes (#38943)

as well as some useful lemmas

This is partly based on code by @scholzhannah
I think this is notable to include, since it is pretty much the only (easy) "topological" sufficient condition for something being a CW complex there is.

Co-authored-by: Batixx <s59fpern@uni-bonn.de>

Author: felixpernegger

Mathlib/Algebra/Group/Fin/Tuple.lean

@@ -103,6 +103,9 @@ variable [Zero α]
 
 @[simp] lemma zero_empty : (0 : Fin 0 → α) = ![] := empty_eq _
 
+@[simp] lemma finZeroElim_eq_zero : (@finZeroElim fun _ ↦ α) = 0 := by
+  rw [Matrix.empty_eq finZeroElim, Matrix.zero_empty]
+
 @[simp] lemma cons_zero_zero : vecCons (0 : α) (0 : Fin n → α) = 0 := by
   ext i; exact i.cases rfl (by simp)
 

Mathlib/Topology/CWComplex/Classical/Basic.lean

@@ -289,6 +289,20 @@ lemma RelCWComplex.map_zero_mem_closedCell [RelCWComplex C D] (n : ℕ) (i : cel
     map n i 0 ∈ closedCell n i :=
   openCell_subset_closedCell _ _ (map_zero_mem_openCell _ _)
 
+lemma RelCWComplex.openCell_nonempty [RelCWComplex C D] (n : ℕ) (j : cell C n) :
+    (openCell n j).Nonempty :=
+  ⟨(map n j) 0, map_zero_mem_openCell n j⟩
+
+lemma RelCWComplex.closedCell_nonempty [RelCWComplex C D] (n : ℕ) (j : cell C n) :
+    (closedCell n j).Nonempty :=
+  ⟨(map n j) 0, map_zero_mem_closedCell n j⟩
+
+/-- If two open cells are equal, so are the underlying cells. -/
+lemma RelCWComplex.openCell_congr [RelCWComplex C D] (n : ℕ) {s t : cell C n}
+    (st : openCell n s = openCell n t) : s = t := by
+  contrapose! st
+  exact (disjoint_openCell_of_ne (by simpa)).ne (openCell_nonempty n s).ne_empty
+
 /-- This is an auxiliary lemma used to prove `RelCWComplex.eq_of_eq_union_iUnion`. -/
 private lemma RelCWComplex.subset_of_eq_union_iUnion [RelCWComplex C D] (I J : Π n, Set (cell C n))
     (hIJ : D ∪ ⋃ (n : ℕ) (j : I n), openCell (C := C) n j =
@@ -1061,4 +1075,45 @@ lemma RelCWComplex.disjoint_interior_base_iUnion_closedCell [T2Space X] [RelCWCo
   simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq,
     iUnion_empty]
 
+/-- A closed discrete subset of a space is a CW complex. -/
+@[reducible, simps -isSimp]
+def CWComplex.OfDiscreteClosed (hD : IsDiscrete D) (Dc : IsClosed D) : CWComplex D where
+  cell n := match n with
+    | 0 => D
+    | (_ + 1) => PEmpty
+  map n i := match n with
+    | 0 => PartialEquiv.single ![] i
+    | (_ + 1) => i.elim
+  source_eq n i := match n with
+    | 0 => by simp [ball, Matrix.empty_eq, eq_univ_iff_forall]
+    | (_ + 1) => i.elim
+  continuousOn n i := match n with
+    | 0 => continuousOn_const
+    | (_ + 1) => i.elim
+  continuousOn_symm n i := match n with
+    | 0 => continuousOn_const
+    | (_ + 1) => i.elim
+  pairwiseDisjoint' := by
+    simp_rw [PairwiseDisjoint, Set.Pairwise, Function.onFun]
+    rintro ⟨_|n, j⟩ _ ⟨_|m, i⟩ _ ne
+    · simp_all [Subtype.coe_injective.ne]
+    · exact i.elim
+    · tauto
+    · exact i.elim
+  mapsTo' n i := match n with
+    | 0 => by simp [Matrix.zero_empty, sphere_eq_empty_of_subsingleton]
+    | (_ + 1) => i.elim
+  closed' A AD _ := isClosed_of_subset_discrete_closed AD hD Dc
+  union' := by
+    apply subset_antisymm (iUnion₂_subset_iff.mpr fun n ↦ by cases n <;> simp)
+    intro x xD
+    simp only [mem_iUnion, mem_image, mem_closedBall, dist_zero_right]
+    refine ⟨0, ?_⟩
+    simpa [-Matrix.zero_empty]
+
+/-- A discrete space is a CW complex. -/
+instance CWComplex.ofDiscreteTopology {X : Type*} [TopologicalSpace X] [DiscreteTopology X] :
+    CWComplex (univ : Set X) :=
+  CWComplex.OfDiscreteClosed IsDiscrete.univ isClosed_univ
+
 end Topology

Mathlib/Topology/Covering/Basic.lean

@@ -497,7 +497,7 @@ variable (f) in
 theorem IsDiscrete.of_openPartialHomeomorph {t : Set E} {x : X}
     (htx : t ⊆ f ⁻¹' {x}) (hf : ∀ e ∈ t, ∃ φ : OpenPartialHomeomorph E X, e ∈ φ.source ∧ φ = f) :
     IsDiscrete t :=
-  isDiscrete_iff_forall_exists_isOpen.mpr fun e he ↦ by
+  isDiscrete_iff_forall_mem_exists_isOpen.mpr fun e he ↦ by
     obtain ⟨φ, hφ, rfl⟩ := hf e he
     exact ⟨_, φ.open_source, subset_antisymm (fun e' he' ↦ φ.injOn he'.1 hφ <|
       (htx he'.2).trans (htx he).symm) <| Set.singleton_subset_iff.mpr ⟨hφ, he⟩⟩

Mathlib/Topology/DiscreteSubset.lean

@@ -65,10 +65,39 @@ lemma discreteTopology_subtype_iff' {S : Set Y} :
   simp [discreteTopology_iff_isOpen_singleton, isOpen_induced_iff, Set.ext_iff]
   grind
 
-theorem isDiscrete_iff_forall_exists_isOpen {S : Set Y} :
-    IsDiscrete S ↔ ∀ y ∈ S, ∃ U, IsOpen U ∧ U ∩ S = {y} := by
+/-- A set `s` is discrete iff for every `y ∈ s` there is an open `u` with `u ∩ s = {y}`.
+See `isDiscrete_iff_forall_subset_exists_isOpen'` for a related version of this with subsets. -/
+theorem isDiscrete_iff_forall_mem_exists_isOpen {s : Set Y} :
+    IsDiscrete s ↔ ∀ y ∈ s, ∃ u, IsOpen u ∧ u ∩ s = {y} := by
   rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff']
 
+@[deprecated (since := "2026-06-24")]
+alias isDiscrete_iff_forall_exists_isOpen := isDiscrete_iff_forall_mem_exists_isOpen
+
+/-- A set `s` is discrete iff for every `t ⊆ s` there is an open `u` with `u ∩ s = t`.
+See `isDiscrete_iff_forall_mem_exists_isOpen` for a similar version of this with singletons. -/
+theorem isDiscrete_iff_forall_subset_exists_isOpen {s : Set X} :
+    IsDiscrete s ↔ ∀ t ⊆ s, ∃ u, IsOpen u ∧ u ∩ s = t := by
+  simp_rw [isDiscrete_iff_discreteTopology, discreteTopology_iff_forall_isOpen,
+    isOpen_induced_iff, ← image_eq_image (Subtype.val_injective), Subtype.image_preimage_coe,
+    Subtype.forall_set_subtype (p := fun t ↦ ∃ u, IsOpen u ∧ s ∩ u = t), inter_comm]
+
+/-- A set `s` is discrete iff for every `t ⊆ s` there is a closed `u` with `u ∩ s = t`. -/
+theorem isDiscrete_iff_forall_mem_exists_isClosed {S : Set X} :
+    IsDiscrete S ↔ ∀ s ⊆ S, ∃ U, IsClosed U ∧ U ∩ S = s := by
+  rw [isDiscrete_iff_forall_subset_exists_isOpen]
+  constructor <;> intro h s sS
+  · obtain ⟨U, Uo, Us⟩ := h (sᶜ ∩ S) inter_subset_right
+    exact ⟨Uᶜ, isClosed_compl_iff.mpr Uo, by rw [left_eq_inter.mpr sS]; simp_all [Set.ext_iff]⟩
+  · obtain ⟨U, Uo, Us⟩ := h (sᶜ ∩ S) inter_subset_right
+    exact ⟨Uᶜ, isOpen_compl_iff.mpr Uo, by rw [left_eq_inter.mpr sS]; simp_all [Set.ext_iff]⟩
+
+theorem isClosed_of_subset_discrete_closed {s t : Set X} (sd : s ⊆ t)
+    (ht : IsDiscrete t) (tc : IsClosed t) : IsClosed s := by
+  obtain ⟨_, rp, rt⟩ := isDiscrete_iff_forall_mem_exists_isClosed.mp ht s sd
+  rw [← rt]
+  exact rp.inter tc
+
 lemma Set.Subsingleton.isDiscrete (hs : s.Subsingleton) : IsDiscrete s :=
   have : Subsingleton s := (Set.subsingleton_coe s).mpr hs
   ⟨inferInstance⟩

Mathlib/Topology/Irreducible.lean

@@ -524,8 +524,8 @@ end
 lemma IsDiscrete.subsingleton_of_isPreirreducible (hs : IsDiscrete s) (hs' : IsPreirreducible s) :
     s.Subsingleton := by
   intro x hxs y hys
-  obtain ⟨U, hU, hUx⟩ := isDiscrete_iff_forall_exists_isOpen.mp hs x hxs
-  obtain ⟨V, hV, hVy⟩ := isDiscrete_iff_forall_exists_isOpen.mp hs y hys
+  obtain ⟨U, hU, hUx⟩ := isDiscrete_iff_forall_mem_exists_isOpen.mp hs x hxs
+  obtain ⟨V, hV, hVy⟩ := isDiscrete_iff_forall_mem_exists_isOpen.mp hs y hys
   obtain ⟨z, hz⟩ := hs' _ _ hU hV ⟨x, by grind⟩ ⟨y, by grind⟩
   exact (hUx.le (by grind)).symm.trans (b := z) (hVy.le (by grind))