hasLineDerivAt_eq_zero — Mathlib

English

Let f: E → ℝ be a function on a real vector space E, and let a ∈ E, b ∈ E. If a is a local extremum of f and the line-derivative of f along the line through a in direction b exists with value f', then f' = 0.

Русский

Пусть f: E → ℝ – функция на вещественном векторном пространстве E, пусть a ∈ E и b ∈ E. Если a является локальным экстремумом f и существует линейная производная по линии через a в направлении b, принимающая значение f', тогда f' = 0.

LaTeX

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

Lean4

theorem hasLineDerivAt_eq_zero (h : IsLocalExtr f a) (hd : HasLineDerivAt ℝ f f' a b) : f' = 0 :=
  IsExtrFilter.hasLineDerivAt_eq_zero h hd <| Continuous.tendsto' (by fun_prop) _ _ (by simp)

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