Theorem intervalIntegral.integral_mono_on_of_le_Ioo

Modification history

2025-01-13 17:41
Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
feat: Estimating a finite sum by an interval integral, for the product of a monotone and an antitone function (#20456) …
Added intervalIntegral.integral_mono_on_of_le_IooView on Github →