hasLineDerivAt_eq_zero — Mathlib

English

If a line through a, in the direction b, is considered, then the line derivative along that line vanishes at a when a is an extremum along that line and the line deriv exists.

Русский

Если рассмотреть линию через a в направлении b, то линейная производная вдоль этой линии в точке a равна нулю при экстремуме вдоль этой линии и существовании линии производной.

LaTeX

$$$\text{IsExtrFilter}(f,l,a) \land \text{HasLineDerivAt}(f,f',a,b) \Rightarrow f' = 0$$$

Lean4

theorem hasLineDerivAt_eq_zero {l : Filter E} (h : IsExtrFilter f l a) (hd : HasLineDerivAt ℝ f f' a b)
    (h' : Tendsto (fun t : ℝ ↦ a + t • b) (𝓝 0) l) : f' = 0 :=
  IsLocalExtr.hasDerivAt_eq_zero (IsExtrFilter.comp_tendsto (by simpa using h) h') hd

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