Theorem Isometry.antilipschitz

Modification history

2026-08-17 18:17
Mathlib/Topology/MetricSpace/Isometry.lean
chore(Analysis): rename CLM.lipschitz, Isometry.lipschitz, Isometry.antilipschitz (#42828) …
Deleted Isometry.antilipschitzView on Github →
2023-03-08 06:41
Mathlib/Topology/MetricSpace/Isometry.lean
feat: port Topology.MetricSpace.Isometry (#2651)
Added Isometry.antilipschitzView on Github →