Theorem TopologicalSpace.Compacts.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.Compacts.mem_singletonView on Github →