Theorem TopologicalSpace.NonemptyCompacts.toCloseds_singleton

Modification history

2025-11-25 09:05
Mathlib/Topology/Sets/Compacts.lean
chore(Topology/Sets/Closeds): add `Singleton` instance to enable `{·}` notation (#32020)
Modified TopologicalSpace.NonemptyCompacts.toCloseds_singletonView on Github →
2025-10-29 12:32
Mathlib/Topology/Sets/Compacts.lean
feat(Topology/Sets): `Singleton` instances for `(Nonempty)Compacts` (#31035)
Added TopologicalSpace.NonemptyCompacts.toCloseds_singletonView on Github →