Theorem ContinuousLinearMap.opNorm_le_of_lipschitz
Modification history
2025-06-20 12:59
Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
feat(MeasureTheory/Measure): bound Hausdorff measure under orthogonal projection (#25759) …
Deleted ContinuousLinearMap.opNorm_le_of_lipschitzView on Github →