Theorem TopologicalSpace.NonemptyCompacts.toCloseds_toCompacts

Modification history

2025-11-16 11:14
Mathlib/Topology/Sets/Compacts.lean
feat(Topology/Sets): add `Compacts.toCloseds` (#31159)
Added TopologicalSpace.NonemptyCompacts.toCloseds_toCompactsView on Github →