feat: singletons are closed in T1 spaces (#14824)

Author: scholzhannah

Mathlib/Data/Set/Subsingleton.lean

@@ -84,6 +84,12 @@ theorem subsingleton_univ_iff : (univ : Set α).Subsingleton ↔ Subsingleton α
   ⟨subsingleton_of_univ_subsingleton, fun h => @subsingleton_univ _ h⟩
 #align set.subsingleton_univ_iff Set.subsingleton_univ_iff
 
+lemma Subsingleton.inter_singleton : (s ∩ {a}).Subsingleton :=
+  Set.subsingleton_of_subset_singleton Set.inter_subset_right
+
+lemma Subsingleton.singleton_inter : ({a} ∩ s).Subsingleton :=
+  Set.subsingleton_of_subset_singleton Set.inter_subset_left
+
 theorem subsingleton_of_subsingleton [Subsingleton α] {s : Set α} : Set.Subsingleton s :=
   subsingleton_univ.anti (subset_univ s)
 #align set.subsingleton_of_subsingleton Set.subsingleton_of_subsingleton

Mathlib/Topology/Separation.lean

@@ -1068,6 +1068,17 @@ theorem SeparationQuotient.t1Space_iff : T1Space (SeparationQuotient X) ↔ R0Sp
     erw [mk_eq_mk, inseparable_iff_specializes_and]
     exact ⟨xspecy, yspecx⟩
 
+lemma Set.Subsingleton.isClosed [T1Space X] {A : Set X} (h : A.Subsingleton) : IsClosed A := by
+  rcases h.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
+  · exact isClosed_empty
+  · exact isClosed_singleton
+
+lemma isClosed_inter_singleton [T1Space X] {A : Set X} {a : X} : IsClosed (A ∩ {a}) :=
+  Subsingleton.inter_singleton.isClosed
+
+lemma isClosed_singleton_inter [T1Space X] {A : Set X} {a : X} : IsClosed ({a} ∩ A) :=
+  Subsingleton.singleton_inter.isClosed
+
 theorem singleton_mem_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X}
     (hx : x ∈ s) : {x} ∈ 𝓝[s] x := by
   have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]