Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes