Commit 2026-09-29 11:56 0493595e

View on Github →

chore(*): rename (anti)lipschitz to (anti)lipschitzWith (#44262) This PR renames

NormedAddGroupHom.lipschitz --> NormedAddGroupHom.lipschitzWith
ContinuousLinearMap.opNorm_le_iff_lipschitz --> ContinuousLinearMap.opNorm_le_iff_lipschitzWith
ContinuousLinearMap.opNorm_le_of_lipschitz --> ContinuousLinearMap.opNorm_le_of_lipschitzWith
ContinuousLinearMap.opNNNorm_le_of_lipschitz --> ContinuousLinearMap.opNNNorm_le_of_lipschitzWith
MeasureTheory.L1.setToL1_lipschitz --> MeasureTheory.L1.setToL1_lipschitzWith

Estimated changes

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

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

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

deleted theorem NormedAddGroupHom.lipschitz

added theorem NormedAddGroupHom.lipschitzWith

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

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

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

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

deleted theorem ContinuousLinearMap.opNorm_le_iff_lipschitz

added theorem ContinuousLinearMap.opNorm_le_iff_lipschitzWith

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

deleted theorem ContinuousLinearMap.opNNNorm_le_of_lipschitz

added theorem ContinuousLinearMap.opNNNorm_le_of_lipschitzWith

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

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

Modified Mathlib/MeasureTheory/Integral/SetToL1/L1.lean

deleted theorem MeasureTheory.L1.setToL1_lipschitz

added theorem MeasureTheory.L1.setToL1_lipschitzWith

Modified Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Star.lean