mathlib3

97492975 - feat(measure_theory/integral/interval_integral): integrability of nonnegative derivatives on open intervals (#14147)

feat(measure_theory/integral/interval_integral): integrability of nonnegative derivatives on open intervals (#14147) Shows that derivatives of continuous functions are integrable when nonnegative. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net> Co-authored-by: loefflerd <d.loeffler.01@cantab.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>