Theorem TopologicalSpace.NonemptyCompacts.mem_singleton

Modification history

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