Theorem TopologicalSpace.Closeds.isEmbedding_singleton

Modification history

2025-11-25 09:05
Mathlib/Topology/UniformSpace/Closeds.lean
chore(Topology/Sets/Closeds): add `Singleton` instance to enable `{·}` notation (#32020)
Modified TopologicalSpace.Closeds.isEmbedding_singletonView on Github →
2025-11-21 11:20
Mathlib/Topology/UniformSpace/Closeds.lean
feat(Topology/UniformSpace/Closeds): uniform continuity of the singleton map (#31868)
Added TopologicalSpace.Closeds.isEmbedding_singletonView on Github →