fderiv_eq_zero — Mathlib

English

If a is a local extremum of f, then the Fréchet derivative of f at a is zero (in the sense of the extended derivative).

Русский

Если a является локальным экстремумом функции f, то производная Фреше в точке a равна нулю (в рамках расширенного определения производной).

LaTeX

$$$\text{IsLocalExtr}(f,a) \Rightarrow fderiv\,\mathbb{R}\,f\,a = 0$$$

Lean4

/-- **Fermat's Theorem**: the derivative of a function at a local extremum equals zero. -/
theorem fderiv_eq_zero (h : IsLocalExtr f a) : fderiv ℝ f a = 0 :=
  h.elim IsLocalMin.fderiv_eq_zero IsLocalMax.fderiv_eq_zero

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