Commit 2025-11-12 13:31 af43db4d

View on Github →

feat(Topology/Sets): injectivity of singleton map (#31379)

Estimated changes

Modified Mathlib/Topology/Sets/Closeds.lean

added theorem TopologicalSpace.Closeds.singleton_inj

added theorem TopologicalSpace.Closeds.singleton_injective

added theorem TopologicalSpace.IrreducibleCloseds.singleton_inj

added theorem TopologicalSpace.IrreducibleCloseds.singleton_injective

Modified Mathlib/Topology/Sets/Compacts.lean

added theorem TopologicalSpace.Compacts.singleton_inj

added theorem TopologicalSpace.Compacts.singleton_injective

added theorem TopologicalSpace.NonemptyCompacts.singleton_inj

added theorem TopologicalSpace.NonemptyCompacts.singleton_injective