lineDeriv_eq_zero — Mathlib

English

If f has local maximum at a, then the line derivative at a vanishes: lineDeriv f a = 0.

Русский

Если у функции f в точке a локальный максимум, то линейная производная в точке a равна нулю.

LaTeX

$$$\operatorname{IsLocalMax}(f,a) \Rightarrow \operatorname{lineDeriv}_{\mathbb{R}}(f,a) = 0$$$

Lean4

theorem lineDeriv_eq_zero (h : IsLocalMax f a) : lineDeriv ℝ f a = 0 :=
  IsLocalExtr.lineDeriv_eq_zero (.inr h)

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