Theorem TopologicalSpace.IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpace

Modification history

2025-12-02 15:26
Mathlib/Topology/Metrizable/CompletelyMetrizable.lean
feat(Topology): IsCompletelyPseudoMetrizable (#31235) …
Added TopologicalSpace.IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpaceView on Github →