mathlib

e7286cac - feat(measure_theory/integral): break up integrals into sums (#18425)

feat(measure_theory/integral): break up integrals into sums (#18425) This shows that if `f` is integrable on each of a countable family of measurable sets in a measure space, and the sum of the integrals of `‖f‖` over these sets converges, then `f` is integrable on their union. We also consider the specific case of breaking up `ℝ` into the union of intervals of length 1.