Commit 2020-09-25 08:21 40f13709
View on Github →chore(measure_theory/bochner_integration): rename/add lemmas, fix docstring (#4249)
- add
integral_nonneg
assuming0 ≤ f
; - rename
integral_nonpos_of_nonpos_ae
tointegral_nonpos_of_ae
; - add
integral_nonpos
assumingf ≤ 0
; - rename
integral_mono
tointegral_mono_ae
; - add
integral_mono
assumingf ≤ g
; - (partially?) fix module docstring.