Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-03 23:18 d04e034a

View on Github →

feat(measure_theory/interval_integral): FTC-2 (#4945) The second fundamental theorem of calculus and supporting lemmas

Estimated changes

Modified src/analysis/calculus/mean_value.lean

added theorem constant_of_deriv_within_zero

added theorem constant_of_has_deriv_right_zero

added theorem eq_of_deriv_within_eq

added theorem eq_of_has_deriv_right_eq

Modified src/measure_theory/interval_integral.lean

added theorem continuous_on.interval_integrable_of_Icc

added theorem interval_integral.continuous_on_integral_of_continuous

added theorem interval_integral.differentiable_on_integral_of_continuous

added theorem interval_integral.integral_deriv_eq_sub

added theorem interval_integral.integral_eq_sub_of_has_deriv_at'

added theorem interval_integral.integral_eq_sub_of_has_deriv_at

added theorem interval_integral.integral_eq_sub_of_has_deriv_right

added theorem interval_integral.integral_eq_sub_of_has_deriv_right_of_le