Commit 2026-08-17 18:17 6a200176

View on Github →

chore(Analysis): rename CLM.lipschitz, Isometry.lipschitz, Isometry.antilipschitz (#42828) This PR renames

ContinuousLinearMap.lipschitz -> ContinuousLinearMap.lipschitzWith
Isometry.lipschitz -> Isometry.lipschitzWith
Isometry.antilipschitz -> Isometry.antilipschitzWith

Estimated changes

Modified Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean

Modified Mathlib/Analysis/BoundedVariation.lean

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Analysis/Complex/Schwarz.lean

Modified Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Modified Mathlib/Analysis/Normed/Affine/Isometry.lean

Modified Mathlib/Analysis/Normed/Group/Pointwise.lean

Modified Mathlib/Analysis/Normed/Module/DoubleDual.lean

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean

Modified Mathlib/Analysis/Normed/Operator/Completeness.lean

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

Modified Mathlib/Analysis/Normed/Operator/NNNorm.lean

deleted theorem ContinuousLinearMap.lipschitz

added theorem ContinuousLinearMap.lipschitzWith

added theorem ContinuousLinearMap.lipschitzWith_apply

deleted theorem ContinuousLinearMap.lipschitz_apply

Modified Mathlib/Analysis/Normed/Operator/NormedSpace.lean

Modified Mathlib/Analysis/Normed/Ring/Lemmas.lean

Modified Mathlib/Analysis/RCLike/BoundedContinuous.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/CompleteOfCompleteLp.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/SpecificCodomains/Pi.lean

Modified Mathlib/Topology/MetricSpace/Completion.lean

Modified Mathlib/Topology/MetricSpace/Cover.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDimension.lean

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean

deleted theorem Isometry.antilipschitz

added theorem Isometry.antilipschitzWith

deleted theorem Isometry.lipschitz

added theorem Isometry.lipschitzWith