mathlib3

30314c22 - fix(measure_theory/interval_integral): generalize some lemmas (#7944)

fix(measure_theory/interval_integral): generalize some lemmas (#7944) The proofs of some lemmas about the integral of a function `f : ℝ → ℝ` also hold for `f : α → ℝ` (with `α` under the usual conditions).