integral_eq_sub_of_hasDeriv_right_of_le_real

English

For real-valued g with differentiability on (a,b) and integrable derivative, ∫_{a}^{b} g'(y) dy = g(b) − g(a).

Русский

Для вещественной функции g с дифференцируемостью на (a,b) и интегрируемой производной выполняется ∫_{a}^{b} g'(y) dy = g(b) − g(a).

LaTeX

$$$\\int_{a}^{b} g'(y)\\,dy = g(b)-g(a)$$$

Lean4

/-- Auxiliary lemma in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`: real version -/
theorem integral_eq_sub_of_hasDeriv_right_of_le_real (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (g'int : IntegrableOn g' (Icc a b)) :
    ∫ y in a..b, g' y = g b - g a :=
  le_antisymm (integral_le_sub_of_hasDeriv_right_of_le hab hcont hderiv g'int fun _ _ => le_rfl)
    (sub_le_integral_of_hasDeriv_right_of_le hab hcont hderiv g'int fun _ _ => le_rfl)

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