Def TopologicalSpace.upgradeIsCompletelyPseudoMetrizable

Modification history

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