Commit 2026-09-09 04:05 a2ba36bc

View on Github →

chore(Topology/MetricSpace/Closeds): rename lemmas about MetricSpace (NonemptyCompacts α) (#42774) These lemmas are moved from the Metric namespace to TopologicalSpace.NonemptyCompacts.

Estimated changes

Modified Mathlib/Topology/MetricSpace/Closeds.lean

deleted theorem Metric.NonemptyCompacts.dist_eq

deleted theorem Metric.lipschitz_infDist

deleted theorem Metric.lipschitz_infDist_set

deleted theorem Metric.uniformContinuous_infDist_Hausdorff_dist

added theorem TopologicalSpace.NonemptyCompacts.dist_eq

added theorem TopologicalSpace.NonemptyCompacts.lipschitz_infDist

added theorem TopologicalSpace.NonemptyCompacts.lipschitz_infDist_const

added theorem TopologicalSpace.NonemptyCompacts.uniformContinuous_infDist