Theorem MonotoneOn.integral_le_sum

Modification history

2023-06-09 13:13
Mathlib/Analysis/SumIntegralComparisons.lean
feat: port Analysis.SumIntegralComparisons (#4902)
Added MonotoneOn.integral_le_sumView on Github →