Theorem TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCloseds

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.NonemptyCompacts.isClosedEmbedding_toCloseds View on Github →