deriv_eq_zero — Mathlib

English

If a is a local maximum of a real-valued function f on ℝ, then the (real) derivative at a vanishes: deriv f a = 0.

Русский

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

LaTeX

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

Lean4

/-- **Fermat's Theorem**: the derivative of a function at a local maximum equals zero. -/
theorem deriv_eq_zero (h : IsLocalMax 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

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