Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-24 08:27 19ae3179

View on Github →

feat(measure_theory/interval_integral): strong version of FTC-2 (#7978) The equality ∫ y in a..b, f' y = f b - f a is currently proved in mathlib assuming that f' is continuous. We weaken the assumption, assuming only that f' is integrable.

Estimated changes