Theorem AntitoneOn.integrableOn_isCompact

Modification history

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