Theorem TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated

Modification history

2025-12-11 10:09
Mathlib/Topology/Metrizable/Basic.lean
refactor: have `MetrizableSpace` not depend on `MetricSpace` (#27946) …
Added TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generatedView on Github →