Theorem TopologicalSpace.NonemptyCompacts.lipschitz_infDist

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_infDistView on Github →