Commit 2024-08-11 23:33 14de5476
View on Github →chore(Integral/Lebesgue): reorganize lintegral_sum_measure (#15502)
Previously, we proved lintegral_sum_measure, then deduced special cases.
The proof of lintegral_sum_measure essentially contained reduction to lintegral_add_measure,
so I prove it first, then deduce lintegral_finset_sum_measure, then lintegral_sum_measure.