integral_deriv_of_contDiffOn_uIcc

English

If f is C^1 on uIcc[a,b], then the same derivative-integral equality holds with appropriate sign conventions.

Русский

Если f C^1 на uIcc[a,b], то равенство производной и разности концов сохраняется.

LaTeX

$$$ContDiffOn \\mathbb{R} 1 f (uIcc a b) \\Rightarrow \\int_a^b deriv f = f(b) - f(a)$$$

Lean4

/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, deriv f y` equals `f b - f a`. -/
theorem integral_deriv_of_contDiffOn_uIcc (h : ContDiffOn ℝ 1 f (uIcc a b)) : ∫ x in a..b, deriv f 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_deriv_of_contDiffOn_Icc h hab
  · simp only [uIcc_of_ge hab.le] at h
    rw [integral_symm, integral_deriv_of_contDiffOn_Icc h hab.le]
    abel

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