Theorem TopologicalSpace.NonemptyCompacts.singleton_inj

Modification history

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