lineDeriv_eq_zero — Mathlib

English

If f has a local maximum at a, and HasLineDerivAt holds for some f' along a line, then f' = 0.

Русский

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

LaTeX

$$$\operatorname{IsLocalMax}(f,a) \land \operatorname{HasLineDerivAt}_{\mathbb{R}}(f,f',a,b) \implies f' = 0$$$

Lean4

theorem lineDeriv_eq_zero (h : IsLocalMin f a) : lineDeriv ℝ f a = 0 :=
  IsLocalExtr.lineDeriv_eq_zero (.inl h)

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