Commit 2021-11-23 13:11 d9e40b44
View on Github →chore(measure_theory/integral): generalize interval_integral.norm_integral_le_integral_norm (#10412)
It was formulated only for functions f : α → ℝ; generalize to f : α → E.
chore(measure_theory/integral): generalize interval_integral.norm_integral_le_integral_norm (#10412)
It was formulated only for functions f : α → ℝ; generalize to f : α → E.