Theorem TopologicalSpace.NonemptyCompacts.singleton_prod_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.singleton_prod_singletonView on Github →