mathlib

3b137447 - chore(measure_theory/integral): more versions of `integral_finset_sum` (#10394)

chore(measure_theory/integral): more versions of `integral_finset_sum` (#10394) * fix assumptions in existing lemmas (`∀ i ∈ s` instead of `∀ i`); * add a version for interval integrals.