Commit 2020-12-19 17:55 154a0242
View on Github →feat(measure_theory/lp_space): add lemmas about the monotonicity of the Lp seminorm (#5395) Also add a lemma mem_Lp.const_smul for a normed space.
feat(measure_theory/lp_space): add lemmas about the monotonicity of the Lp seminorm (#5395) Also add a lemma mem_Lp.const_smul for a normed space.