mathlib

29d0c63d - feat(measure_theory): add a few integration-related lemmas (#7821)

feat(measure_theory): add a few integration-related lemmas (#7821) These are lemmas I proved while working on #7164. Some of them are actually not used anymore in that PR because I'm refactoring it, but I thought they would be useful anyway, so here there are.