feat(topology/sets/closeds): atoms in a t1_space are singletons (#16721)
feat(topology/sets/closeds): atoms in a t1_space are singletons (#16721)

This is helpful to show that maximal ideals of `C(X, 𝕜)` with `X` compact Hausdorff and `𝕜` either `ℝ` or `ℂ` correspond to complements of singletons with respect to the Galois connection between `continuous_map.ideal_to_set` and `continuous_map.set_to_ideal`.





leanprover-community/mathlib,leanprover-community/mathlib