mathlib3
4afd667f - feat(measure_theory/integral): add `integral_sum_measure` (#12090)

Commit

3 years ago

feat(measure_theory/integral): add `integral_sum_measure` (#12090) Also add supporting lemmas about finite and infinite sums of measures.

Author

urkud

Parents