Theorem TopologicalSpace.NonemptyCompacts.lipschitz_infDist_const

Modification history

2026-09-09 04:05
Mathlib/Topology/MetricSpace/Closeds.lean
chore(Topology/MetricSpace/Closeds): rename lemmas about `MetricSpace (NonemptyCompacts α)` (#42774) …
Added TopologicalSpace.NonemptyCompacts.lipschitz_infDist_constView on Github →