Theorem TopologicalSpace.Closeds.isClosed_setOf_totallyBounded

Modification history

2026-03-25 13:40

Mathlib/Topology/UniformSpace/Closeds.lean

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

Added TopologicalSpace.Closeds.isClosed_setOf_totallyBounded View on Github →