Commit 2025-11-21 11:20 8d63eaa7

View on Github →

feat(Topology/UniformSpace/Closeds): uniform continuity of the singleton map (#31868)

Estimated changes

Modified Mathlib/Topology/UniformSpace/Closeds.lean

added theorem TopologicalSpace.Closeds.continuous_singleton

added theorem TopologicalSpace.Closeds.isClosedEmbedding_singleton

added theorem TopologicalSpace.Closeds.isEmbedding_singleton

added theorem TopologicalSpace.Closeds.isUniformEmbedding_singleton

added theorem TopologicalSpace.Closeds.uniformContinuous_singleton

added theorem TopologicalSpace.Compacts.isUniformEmbedding_singleton

added theorem TopologicalSpace.Compacts.uniformContinuous_singleton

added theorem TopologicalSpace.NonemptyCompacts.isUniformEmbedding_singleton

added theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_singleton

added theorem UniformSpace.hausdorff.isClopen_singleton_empty

added theorem UniformSpace.hausdorff.isClosedEmbedding_singleton

added theorem UniformSpace.hausdorff.isUniformEmbedding_singleton

added theorem singleton_mem_hausdorffEntourage