Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-20 10:38 d9a8d6e5

View on Github →

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.

Estimated changes