exists_deriv_eq_slope' — Mathlib

English

There exists c ∈ Ioo(a,b) with deriv f c equal to slope f a b, i.e., deriv f c = slope f a b.

Русский

Существует c ∈ Ioo(a,b) такое, что deriv f c равно наклону отрезка f(a) к f(b).

LaTeX

$$$\\exists c\\in I^{oo}_{a,b},\\; \\mathrm{deriv}\\ f\\ c = \\operatorname{slope} f\\ a\\ b$$$

Lean4

/-- Lagrange's **Mean Value Theorem**, `deriv` version. -/
theorem exists_deriv_eq_slope' : ∃ c ∈ Ioo a b, deriv f c = slope f a b :=
  by
  rw [slope_def_field]
  exact exists_deriv_eq_slope f hab hfc hfd

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