hasFDerivAt_eq_zero — Mathlib

English

Fermat's theorem: if f has a local minimum at a, then HasFDerivAt f f' a implies f' = 0.

Русский

Теорема Ферма: если у f локальный минимум в a и существует производная, то производная равна нулю.

LaTeX

$$$ f' = 0 $$$

Lean4

/-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero. -/
theorem hasFDerivAt_eq_zero (h : IsLocalMin f a) (hf : HasFDerivAt f f' a) : f' = 0 :=
  by
  ext y
  apply (h.on univ).hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt <;> rw [posTangentConeAt_univ] <;> apply mem_univ

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