Theorem ContinuousLinearMap.lipschitzWith

Modification history

2026-08-17 18:17
Mathlib/Analysis/Normed/Operator/NNNorm.lean
chore(Analysis): rename CLM.lipschitz, Isometry.lipschitz, Isometry.antilipschitz (#42828) …
Added ContinuousLinearMap.lipschitzWithView on Github →