Commit 2025-04-15 07:00 e7b8f4e1

View on Github →

feat(Topology): closure of subsingleton is self (#24062) Proves Set.Subsingleton.closure_eq

Estimated changes

Modified Mathlib/Topology/Separation/Basic.lean

added theorem Set.Subsingleton.closure_eq

modified theorem Set.Subsingleton.isClosed