Commit 2023-02-17 06:57 e7286cac

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.