Theorem integral_le_sum_Ico_of_le

Modification history

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