Commit 2021-06-07 01:12 29d0c63d
View on Github →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.