Theorem TopologicalSpace.NonemptyCompacts.toCompacts_singleton

Modification history

2025-11-21 11:20
Mathlib/Topology/Sets/Compacts.lean
chore(Topology/Sets): use prefix naming for `toCompacts` in `simps` (#31591)
Deleted TopologicalSpace.NonemptyCompacts.toCompacts_singletonView on Github →
2025-10-29 12:32
Mathlib/Topology/Sets/Compacts.lean
feat(Topology/Sets): `Singleton` instances for `(Nonempty)Compacts` (#31035)
Added TopologicalSpace.NonemptyCompacts.toCompacts_singletonView on Github →