hasDerivAt_eq_zero — Mathlib

English

Let f: ℝ → ℝ. If a is a local minimum of f and f is differentiable at a with derivative f', then f' = 0.

Русский

Пусть f: ℝ → ℝ. Если a является локальным минимумом f и f дифференцируема в a с производной f', то f' = 0.

LaTeX

$$$\text{IsLocalMin}(f,a) \land \text{HasDerivAt}(f,f',a) \Rightarrow f' = 0$$$

Lean4

/-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero. -/
theorem hasDerivAt_eq_zero (h : IsLocalMin f a) (hf : HasDerivAt f f' a) : f' = 0 := by
  simpa using DFunLike.congr_fun (h.hasFDerivAt_eq_zero (hasDerivAt_iff_hasFDerivAt.1 hf)) 1

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