From 0150f3cbc1f208cb6f7e7de7fce69f3241f25920 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 20 Sep 2026 16:01:19 +0200 Subject: [PATCH] chore: rename AffineIsometry{Equiv}.{anti}lipschitz Part of #42869. --- Mathlib/Analysis/Normed/Affine/Isometry.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/Normed/Affine/Isometry.lean b/Mathlib/Analysis/Normed/Affine/Isometry.lean index 7618424e17a169..2f16e812a7755c 100644 --- a/Mathlib/Analysis/Normed/Affine/Isometry.lean +++ b/Mathlib/Analysis/Normed/Affine/Isometry.lean @@ -154,12 +154,15 @@ theorem map_eq_iff {x y : P₁'} : f₁ x = f₁ y ↔ x = y := theorem map_ne {x y : P₁'} (h : x ≠ y) : f₁ x ≠ f₁ y := f₁.injective.ne h -protected theorem lipschitz : LipschitzWith 1 f := +protected theorem lipschitzWith : LipschitzWith 1 f := f.isometry.lipschitzWith -protected theorem antilipschitz : AntilipschitzWith 1 f := +protected theorem antilipschitzWith : AntilipschitzWith 1 f := f.isometry.antilipschitzWith +@[deprecated (since := "2026-09-20")] alias lipschitz := AffineIsometry.lipschitzWith +@[deprecated (since := "2026-09-20")] alias antilipschitz := AffineIsometry.antilipschitzWith + @[continuity] protected theorem continuous : Continuous f := f.isometry.continuous @@ -634,12 +637,15 @@ theorem map_eq_iff {x y : P} : e x = e y ↔ x = y := theorem map_ne {x y : P} (h : x ≠ y) : e x ≠ e y := e.injective.ne h -protected theorem lipschitz : LipschitzWith 1 e := +protected theorem lipschitzWith : LipschitzWith 1 e := e.isometry.lipschitzWith -protected theorem antilipschitz : AntilipschitzWith 1 e := +protected theorem antilipschitzWith : AntilipschitzWith 1 e := e.isometry.antilipschitzWith +@[deprecated (since := "2026-09-20")] alias lipschitz := AffineIsometryEquiv.lipschitzWith +@[deprecated (since := "2026-09-20")] alias antilipschitz := AffineIsometryEquiv.antilipschitzWith + @[simp] theorem ediam_image (s : Set P) : ediam (e '' s) = ediam s := e.isometry.ediam_image s