Commit 2026-03-25 13:40 1c4c89f8

View on Github →

feat(Topology/UniformSpace/Closeds): (Nonempty)Compacts.toCloseds is a closed embedding (#34270)

Estimated changes

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Modified Mathlib/Topology/UniformSpace/Closeds.lean

added theorem TopologicalSpace.Closeds.isClosed_setOf_totallyBounded

added theorem TopologicalSpace.Compacts.isClosedEmbedding_toCloseds

added theorem TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCloseds

added theorem UniformSpace.hausdorff.isClosed_setOf_totallyBounded