Theorem TopologicalSpace.NonemptyCompacts.mem_toCloseds

Modification history

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