exists_deriv_eq_slope — Mathlib

English

There exists c ∈ (a,b) such that deriv f c equals the slope (f(b)−f(a))/(b−a).

Русский

Существует c ∈ (a,b), для которого производная f в c равна наклону секущей: f′(c) = (f(b)−f(a))/(b−a).

LaTeX

$$$\\exists c\\in I^{o}_{a,b},\\; \\mathrm{deriv}\\ f\\ c = \\dfrac{f(b)-f(a)}{b-a}$$$

Lean4

/-- Lagrange's **Mean Value Theorem**, `deriv` version. -/
theorem exists_deriv_eq_slope : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
  exists_hasDerivAt_eq_slope f (deriv f) hab hfc fun x hx =>
    ((hfd x hx).differentiableAt <| IsOpen.mem_nhds isOpen_Ioo hx).hasDerivAt

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