mathlib

d9a8d6e5 - feat(topology/separation): Finite sets in T2 spaces (#12845)

feat(topology/separation): Finite sets in T2 spaces (#12845) We prove the following theorem: given a finite set in a T2 space, one can choose an open set around each point so that these are pairwise disjoint.