Theorem enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc

Modification history

2025-06-16 06:44
Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean
feat: easier to use FTC-2 versions for `C^1` functions (#25769)
Added enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_IccView on Github →