Theorem ContinuousLinearMap.opNNNorm_le_of_lipschitzWith

Modification history

2026-09-29 11:56
Mathlib/Analysis/Normed/Operator/NNNorm.lean
chore(*): rename (anti)lipschitz to (anti)lipschitzWith (#44262) …
Added ContinuousLinearMap.opNNNorm_le_of_lipschitzWithView on Github →