Commit 2025-03-18 14:37 c58b874b

View on Github →

feat: completely metrizable spaces (#22926) Introduce the notion of completely metrizable spaces and refactor PolishSpace using it.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

Modified Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

Modified Mathlib/Topology/MetricSpace/Perfect.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean

deleted theorem complete_polishSpaceMetric

deleted def polishSpaceMetric

deleted def upgradePolishSpace

Created Mathlib/Topology/Metrizable/CompletelyMetrizable.lean

added theorem IsClosed.isCompletelyMetrizableSpace

added theorem TopologicalSpace.complete_completelyMetrizableMetric

added def TopologicalSpace.upgradeIsCompletelyMetrizable

added theorem Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace