Theorem MeasureTheory.integral_monotoneOn_of_integrand_ae

Modification history

2025-05-07 04:11
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
feat(MeasureTheory): integral is monotone/convex if the integrand is monotone/convex (#24341) …
Added MeasureTheory.integral_monotoneOn_of_integrand_aeView on Github →