mathlib3
2f1f34a9 - feat(measure_theory/lp_space): add `mem_Lp.mono_measure` (#7927)

Commit

4 years ago

feat(measure_theory/lp_space): add `mem_Lp.mono_measure` (#7927) also add monotonicity lemmas wrt the measure for `snorm'`, `snorm_ess_sup` and `snorm`.

Author

RemyDegenne

Parents

5f8cc8eb

mathlib3 2f1f34a9 - feat(measure_theory/lp_space): add `mem_Lp.mono_measure` (#7927)

mathlib3
2f1f34a9 - feat(measure_theory/lp_space): add `mem_Lp.mono_measure` (#7927)