Commit 2025-11-25 09:05 9c72f58d

View on Github →

chore(Topology/Sets/Closeds): add Singleton instance to enable {·} notation (#32020)

Estimated changes

Modified Mathlib/Topology/ContinuousMap/Ideals.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean

modified theorem EMetric.Closeds.isometry_singleton

Modified Mathlib/Topology/Sets/Closeds.lean

modified theorem TopologicalSpace.Closeds.mem_singleton

added theorem TopologicalSpace.Closeds.mk_singleton

deleted def TopologicalSpace.Closeds.singleton

modified theorem TopologicalSpace.Closeds.singleton_inj

modified theorem TopologicalSpace.Closeds.singleton_injective

modified theorem TopologicalSpace.IrreducibleCloseds.mem_singleton

added theorem TopologicalSpace.IrreducibleCloseds.mk_singleton

deleted def TopologicalSpace.IrreducibleCloseds.singleton

modified theorem TopologicalSpace.IrreducibleCloseds.singleton_inj

modified theorem TopologicalSpace.IrreducibleCloseds.singleton_injective

Modified Mathlib/Topology/Sets/Compacts.lean

modified theorem TopologicalSpace.Compacts.toCloseds_singleton

modified theorem TopologicalSpace.NonemptyCompacts.toCloseds_singleton

Modified Mathlib/Topology/UniformSpace/Closeds.lean

modified theorem TopologicalSpace.Closeds.continuous_singleton

modified theorem TopologicalSpace.Closeds.isClosedEmbedding_singleton

modified theorem TopologicalSpace.Closeds.isEmbedding_singleton

modified theorem TopologicalSpace.Closeds.isUniformEmbedding_singleton

modified theorem TopologicalSpace.Closeds.uniformContinuous_singleton