feat: Finite product of Alexandrov-discrete spaces is Alexandrov-discrete (#27018)

Author: Komyyy

Mathlib/Order/Filter/Ker.lean

@@ -68,4 +68,13 @@ theorem ker_sSup (S : Set (Filter α)) : ker (sSup S) = ⋃ f ∈ S, ker f := by
 theorem ker_sup (f g : Filter α) : ker (f ⊔ g) = ker f ∪ ker g := by
   rw [← sSup_pair, ker_sSup, biUnion_pair]
 
+@[simp]
+lemma ker_prod (f : Filter α) (g : Filter β) : ker (f ×ˢ g) = ker f ×ˢ ker g := by
+  simp [Set.prod_eq, Filter.prod_eq_inf]
+
+@[simp]
+lemma ker_pi {ι : Type*} {α : ι → Type*} (f : (i : ι) → Filter (α i)) :
+    ker (Filter.pi f) = univ.pi (fun i => ker (f i)) := by
+  simp [Set.pi_def, Filter.pi]
+
 end Filter

Mathlib/Topology/AlexandrovDiscrete.lean

@@ -21,10 +21,6 @@ minimal neighborhood, which we call the *neighborhoods kernel* of the set.
 
 * `AlexandrovDiscrete`: Prop-valued typeclass for a topological space to be Alexandrov-discrete
 
-## TODO
-
-Finite product of Alexandrov-discrete spaces is Alexandrov-discrete.
-
 ## Tags
 
 Alexandroff, discrete, finitely generated, fg space
@@ -34,6 +30,7 @@ open Filter Set TopologicalSpace Topology
 
 /-- A topological space is **Alexandrov-discrete** or **finitely generated** if the intersection of
 a family of open sets is open. -/
+@[mk_iff]
 class AlexandrovDiscrete (α : Type*) [TopologicalSpace α] : Prop where
   /-- The intersection of a family of open sets is an open set. Use `isOpen_sInter` in the root
   namespace instead. -/
@@ -43,6 +40,12 @@ variable {ι : Sort*} {κ : ι → Sort*} {α β : Type*}
 section
 variable [TopologicalSpace α] [TopologicalSpace β]
 
+lemma alexandrovDiscrete_iff_isClosed :
+    AlexandrovDiscrete α ↔ ∀ S : Set (Set α), (∀ s ∈ S, IsClosed s) → IsClosed (⋃₀ S) := by
+  conv_lhs => tactic =>
+    simp_rw +singlePass [alexandrovDiscrete_iff, compl_surjective.image_surjective.forall,
+      forall_mem_image, ← compl_sUnion, isOpen_compl_iff]
+
 instance DiscreteTopology.toAlexandrovDiscrete [DiscreteTopology α] : AlexandrovDiscrete α where
   isOpen_sInter _ _ := isOpen_discrete _
 
@@ -61,8 +64,8 @@ lemma isOpen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsOpen (f i j
     IsOpen (⋂ i, ⋂ j, f i j) :=
   isOpen_iInter fun _ ↦ isOpen_iInter <| hf _
 
-lemma isClosed_sUnion (hS : ∀ s ∈ S, IsClosed s) : IsClosed (⋃₀ S) := by
-  simp only [← isOpen_compl_iff, compl_sUnion] at hS ⊢; exact isOpen_sInter <| forall_mem_image.2 hS
+lemma isClosed_sUnion (hS : ∀ s ∈ S, IsClosed s) : IsClosed (⋃₀ S) :=
+  alexandrovDiscrete_iff_isClosed.mp inferInstance S hS
 
 lemma isClosed_iUnion (hf : ∀ i, IsClosed (f i)) : IsClosed (⋃ i, f i) :=
   isClosed_sUnion <| forall_mem_range.2 hf
@@ -196,6 +199,18 @@ lemma isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s
   simp only [← nhdsKer_subset_iff_isOpen, Set.subset_def, mem_nhdsKer_iff_specializes, exists_imp,
     and_imp, @forall_swap (_ ⤳ _)]
 
+omit [AlexandrovDiscrete α] in
+lemma alexandrovDiscrete_iff_nhds : AlexandrovDiscrete α ↔ (∀ a : α, 𝓝 a = 𝓟 (nhdsKer {a})) where
+  mp _ a := principal_nhdsKer_singleton a |>.symm
+  mpr hα := by
+    simp only [alexandrovDiscrete_iff_isClosed, isClosed_iff_clusterPt, ClusterPt, funext hα,
+      inf_principal, principal_neBot_iff]
+    intro S hS a ha
+    rw [sUnion_eq_biUnion, inter_iUnion₂, nonempty_biUnion] at ha
+    obtain ⟨s, hs, has⟩ := ha
+    specialize hS s hs a has
+    exact mem_sUnion_of_mem hS hs
+
 lemma alexandrovDiscrete_coinduced {β : Type*} {f : α → β} :
     @AlexandrovDiscrete β (coinduced f ‹_›) :=
   @AlexandrovDiscrete.mk β (coinduced f ‹_›) fun S hS ↦ by
@@ -222,4 +237,14 @@ instance Sigma.instAlexandrovDiscrete {ι : Type*} {X : ι → Type*} [∀ i, To
     [∀ i, AlexandrovDiscrete (X i)] : AlexandrovDiscrete (Σ i, X i) :=
   alexandrovDiscrete_iSup fun _ ↦ alexandrovDiscrete_coinduced
 
+instance Prod.instAlexandrovDiscrete : AlexandrovDiscrete (α × β) := by
+  simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
+    prod_principal_principal, nhdsKer_pair, forall_true_iff]
+
+instance Pi.instAlexandrovDiscreteOfFinite {ι : Type*} [Finite ι] {X : ι → Type*}
+    [Π i, TopologicalSpace (X i)] [∀ i, AlexandrovDiscrete (X i)] :
+    AlexandrovDiscrete (Π i, X i) := by
+  simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
+    pi_principal, nhdsKer_singleton_pi, forall_true_iff]
+
 end

Mathlib/Topology/NhdsKer.lean

@@ -71,6 +71,10 @@ theorem nhdsKer_iUnion (s : ι → Set X) : nhdsKer (⋃ i, s i) = ⋃ i, nhdsKe
 
 @[deprecated (since := "2025-07-09")] alias exterior_iUnion := nhdsKer_iUnion
 
+theorem nhdsKer_biUnion {ι : Type*} (s : Set ι) (t : ι → Set X) :
+    nhdsKer (⋃ i ∈ s, t i) = ⋃ i ∈ s, nhdsKer (t i) := by
+  simp only [nhdsKer_iUnion]
+
 @[simp]
 theorem nhdsKer_union (s t : Set X) : nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t := by
   simp only [nhdsKer, nhdsSet_union, ker_sup]
@@ -160,3 +164,33 @@ theorem nhdsKer_sInter_subset {s : Set (Set X)} : nhdsKer (⋂₀ s) ⊆ ⋂ x 
   simp only [nhdsKer_eq_nhdsKer_iff_nhdsSet, nhdsSet_nhdsKer]
 
 @[deprecated (since := "2025-07-09")] alias exterior_exterior := nhdsKer_nhdsKer
+
+lemma nhdsKer_pair {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+    (x : X) (y : Y) : nhdsKer {(x, y)} = nhdsKer {x} ×ˢ nhdsKer {y} := by
+  simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_prod_eq, ker_prod]
+
+lemma nhdsKer_prod {Y : Type*} [TopologicalSpace Y] (s : Set X) (t : Set Y) :
+    nhdsKer (s ×ˢ t) = nhdsKer s ×ˢ nhdsKer t := calc
+  _ = ⋃ (p ∈ s ×ˢ t), nhdsKer {p} := by
+    conv_lhs => rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]
+  _ = ⋃ (p ∈ s ×ˢ t), nhdsKer {p.1} ×ˢ nhdsKer {p.2} := by
+    congr! with ⟨x, y⟩ _; rw [nhdsKer_pair]
+  _ = (⋃ x ∈ s, nhdsKer {x}) ×ˢ (⋃ y ∈ t, nhdsKer {y}) :=
+    biUnion_prod s t (fun x => nhdsKer {x}) (fun y => nhdsKer {y})
+  _ = nhdsKer s ×ˢ nhdsKer t := by
+    simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]
+
+lemma nhdsKer_singleton_pi {ι : Type*} {X : ι → Type*} [Π (i : ι), TopologicalSpace (X i)]
+    (p : Π (i : ι), X i) : nhdsKer {p} = univ.pi (fun i => nhdsKer {p i}) := by
+  simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_pi, ker_pi]
+
+lemma nhdsKer_pi {ι : Type*} {X : ι → Type*} [Π (i : ι), TopologicalSpace (X i)]
+    (s : Π (i : ι), Set (X i)) : nhdsKer (univ.pi s) = univ.pi (fun i => nhdsKer (s i)) := calc
+  _ = ⋃ (p ∈ univ.pi s), nhdsKer {p} := by
+    conv_lhs => rw [← biUnion_of_singleton (univ.pi s), nhdsKer_biUnion]
+  _ = ⋃ (p ∈ univ.pi s), univ.pi fun i => nhdsKer {p i} := by
+    congr! with p _; rw [nhdsKer_singleton_pi]
+  _ = univ.pi fun i => ⋃ x ∈ s i, nhdsKer {x} :=
+    biUnion_univ_pi s fun i x => nhdsKer {x}
+  _ = univ.pi (fun i => nhdsKer (s i)) := by
+    simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]