Theorem TopologicalSpace.Compacts.map_singleton

Modification history

2025-10-29 12:32
Mathlib/Topology/Sets/Compacts.lean
feat(Topology/Sets): `Singleton` instances for `(Nonempty)Compacts` (#31035)
Added TopologicalSpace.Compacts.map_singletonView on Github →