Theorem TopologicalSpace.Compacts.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.Compacts.toCloseds_singletonView on Github →
2025-11-16 11:14
Mathlib/Topology/Sets/Compacts.lean
feat(Topology/Sets): add `Compacts.toCloseds` (#31159)
Added TopologicalSpace.Compacts.toCloseds_singletonView on Github →