deriv_eq_zero — Mathlib

English

If a is a local minimum of f, then the derivative at a is zero: deriv f a = 0.

Русский

Если a — локальный минимум функции f, то производная в a равна нулю: deriv f a = 0.

LaTeX

$$$\mathrm{IsLocalMin}(f,a) \Rightarrow \mathrm{deriv}(f,a) = 0$$$

Lean4

/-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero. -/
theorem deriv_eq_zero (h : IsLocalMin f a) : deriv f a = 0 := by
  classical
    exact
    if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt else deriv_zero_of_not_differentiableAt hf

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