Theorem ContinuousLinearMap.opNorm_le_iff_lipschitz

Modification history

2026-09-29 11:56
Mathlib/Analysis/Normed/Operator/Basic.lean
chore(*): rename (anti)lipschitz to (anti)lipschitzWith (#44262) …
Deleted ContinuousLinearMap.opNorm_le_iff_lipschitzView on Github →
2025-06-20 12:59
Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
feat(MeasureTheory/Measure): bound Hausdorff measure under orthogonal projection (#25759) …
Added ContinuousLinearMap.opNorm_le_iff_lipschitzView on Github →