Theorem intervalIntegral.differentiable_integral_of_continuous

Modification history

2025-07-04 15:22
Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean
feat: monotonicity of `lineMap` (#26502) …
Added intervalIntegral.differentiable_integral_of_continuousView on Github →