Theorem TopologicalSpace.complete_completelyPseudoMetrizableMetric

Modification history

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