hasFDerivAt_eq_zero — Mathlib

English

Let f : E → ℝ be as above and suppose a is a local extremum of f. If f has a Fréchet derivative f' at a, then f' = 0.

Русский

Пусть f : E → ℝ имеет локальный экстремум в точке a. Если в точке a существуeт производная Фреше f' , то f' = 0.

LaTeX

$$$\text{IsLocalExtr}(f,a) \land \text{HasFDerivAt}(f,f',a) \Rightarrow f' = 0$$$

Lean4

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

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