mathlib3
d9e40b44 - chore(measure_theory/integral): generalize `interval_integral.norm_integral_le_integral_norm` (#10412)

Commit

4 years ago

chore(measure_theory/integral): generalize `interval_integral.norm_integral_le_integral_norm` (#10412) It was formulated only for functions `f : α → ℝ`; generalize to `f : α → E`.

Author

urkud

Parents

28177886

mathlib3 d9e40b44 - chore(measure_theory/integral): generalize `interval_integral.norm_integral_le_integral_norm` (#10412)

mathlib3
d9e40b44 - chore(measure_theory/integral): generalize `interval_integral.norm_integral_le_integral_norm` (#10412)