Commit 2021-12-11 21:21 f9fff7c6
View on Github →feat(measure_theory): integral is mono in measure (#10721)
- Bochner integral of a nonnegative function is monotone in measure;
- set integral of a nonnegative function is monotone in set (generalize existing lemma);
- interval integral of a nonnegative function is monotone in interval.