integral_derivWithin_uIcc_of_contDiffOn_uIcc

English

If a vector-valued function f: R → E is continuously differentiable on the closed interval [a,b], then the integral of its derivative over [a,b] equals f(b) − f(a).

Русский

Пусть f: ℝ → E является непрерывно дифференцируемой на отрезке [a,b]. Тогда ∫_a^b f'(x) dx = f(b) − f(a).

LaTeX

$$$\\displaystyle \\int_{a}^{b} f'(x) \\, dx = f(b) - f(a),$$$

Lean4

/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, derivWithin f (uIcc a b) y` equals `f b - f a`. -/
theorem integral_derivWithin_uIcc_of_contDiffOn_uIcc (h : ContDiffOn ℝ 1 f (uIcc a b)) :
    ∫ x in a..b, derivWithin f (uIcc a b) x = f b - f a :=
  by
  rcases le_or_gt a b with hab | hab
  · simp only [uIcc_of_le hab] at h ⊢
    exact integral_derivWithin_Icc_of_contDiffOn_Icc h hab
  · simp only [uIcc_of_ge hab.le] at h ⊢
    rw [integral_symm, integral_derivWithin_Icc_of_contDiffOn_Icc h hab.le]
    abel

Похожие утверждения