Theorem Isometry.lipschitzWith

Modification history

2026-08-17 18:17
Mathlib/Topology/MetricSpace/Isometry.lean
chore(Analysis): rename CLM.lipschitz, Isometry.lipschitz, Isometry.antilipschitz (#42828) …
Added Isometry.lipschitzWithView on Github →