lineDerivWithin_eq_zero — Mathlib

English

If f is extr on s at a, then the line derivative within s along a, b is zero whenever the appropriate line derivative exists.

Русский

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

LaTeX

$$$\text{IsExtrOn}(f,s,a) \land \text{HasLineDerivWithinAt}(f,f',s,a,b) \Rightarrow f' = 0$$$

Lean4

theorem lineDerivWithin_eq_zero (h : IsExtrOn f s a) (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) :
    lineDerivWithin ℝ f s a b = 0 := by
  classical
    exact
    if hd : LineDifferentiableWithinAt ℝ f s a b then h.hasLineDerivWithinAt_eq_zero hd.hasLineDerivWithinAt h'
    else lineDerivWithin_zero_of_not_lineDifferentiableWithinAt hd

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