Commit 2025-12-11 10:09 6014a431

View on Github →

refactor: have MetrizableSpace not depend on MetricSpace (#27946) Some theorems for uniform spaces with a countably generated uniformity do not mention their uniformity in any of the hypotheses or the conclusion (for example UniformSpace.isCompact_iff_isSeqCompact). This PR allows those theorems to be stated for (pseudo)metrizable spaces without importing the real numbers.

  • Use TopologicalSpace.pseudoMetrizableSpaceUniformity to endow a pseudometrizable space with a compatible uniformity, and use TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated to show that this is countably generated.
  • TopologicalSpace.pseudoMetrizableSpacePseudoMetric and TopologicalSpace.metrizableSpaceMetric have been moved to Mathlib/Topology/Metrizable/Uniformity.lean. See also #2032

Estimated changes