Commit 2025-11-16 11:14 db9dae86

View on Github →

feat(Topology/Sets): add Compacts.toCloseds (#31159)

Estimated changes

Modified Mathlib/Topology/Sets/Compacts.lean

added theorem TopologicalSpace.Compacts.mem_toCloseds

added def TopologicalSpace.Compacts.toCloseds

added theorem TopologicalSpace.Compacts.toCloseds_singleton

added theorem TopologicalSpace.NonemptyCompacts.mem_toCloseds

added theorem TopologicalSpace.NonemptyCompacts.mem_toCompacts

added theorem TopologicalSpace.NonemptyCompacts.toCloseds_toCompacts