Commit 2025-11-02 21:27 8387c032
View on Github →refactor(Topology): cleaner way to get metric spaces from emetric spaces (#29321) Change EMetricSpace.toMetricSpaceOfDist in Mathlib/Topology/MetricSpace/Basic and PseudoEMetricSpace.toPseudoMetricSpaceOfDist in Mathlib/Topology/MetricSpace/Pseudo/Defs to require nonnegativity of given distance function rather than finiteness of old edistance.