Theorem MeasureTheory.Lp.norm_LpToLpOfMeasureLeSMul_le

Modification history

2026-07-02 18:37
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
feat: linear map from `L^p (mu)` to `L^p (nu)` when `nu` is bounded by a multiple of `mu` (#40811)
Added MeasureTheory.Lp.norm_LpToLpOfMeasureLeSMul_leView on Github →