mathlib

2e348d40 - 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`.