Commit 2024-07-17 18:39 a79d64d3

View on Github →

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

Estimated changes

Modified Mathlib/Data/Set/Subsingleton.lean

added theorem Set.Subsingleton.inter_singleton

added theorem Set.Subsingleton.singleton_inter

Modified Mathlib/Topology/Separation.lean

added theorem Set.Subsingleton.isClosed

added theorem isClosed_inter_singleton

added theorem isClosed_singleton_inter