hasLineDerivAt_eq_zero — Mathlib

English

If a function is extr on a set along a line with a line derivative, the derivative along that line is zero provided the line remains in the set near a.

Русский

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

LaTeX

$$$\text{IsExtrOn}(f,s,a) \land \text{HasLineDerivAt}(f,f',a,b) \land \forall^{\mathrm{frequently}} t, a+ t b \in s \Rightarrow f' = 0$$$

Lean4

theorem hasLineDerivAt_eq_zero (h : IsExtrOn f s a) (hd : HasLineDerivAt ℝ f f' a b)
    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
  IsExtrFilter.hasLineDerivAt_eq_zero h hd <| tendsto_principal.2 h'

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