Commit 2021-06-14 21:50 8377a1fc
View on Github →feat(measure_theory/lp_space): add snorm_le_snorm_mul_rpow_measure_univ (#7926)
There were already versions of this lemma for snorm' and snorm_ess_sup. The new lemma collates these into a statement about snorm.