exists_hasDerivAt_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, `HasDerivAt` version -/
theorem exists_hasDerivAt_eq_slope : ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a) :=
  by
  obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Ioo a b, (b - a) * f' c = (f b - f a) * 1 :=
    exists_ratio_hasDerivAt_eq_ratio_slope f f' hab hfc hff' id 1 continuousOn_id fun x _ => hasDerivAt_id x
  use c, cmem
  rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc

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