Theorem TopologicalSpace.NonemptyCompacts.singleton_injective

Modification history

2025-11-12 13:31
Mathlib/Topology/Sets/Compacts.lean
feat(Topology/Sets): injectivity of singleton map (#31379)
Added TopologicalSpace.NonemptyCompacts.singleton_injectiveView on Github →