hasLineDerivWithinAt_eq_zero — Mathlib

English

If IsMaxOn f s a and HasLineDerivWithinAt f f' s a b with a rightward approach inside s, then f' = 0.

Русский

Если IsMaxOn f s a и существует HasLineDerivWithinAt f f' s a b при приближении справа внутри s, то f' = 0.

LaTeX

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

Lean4

theorem hasLineDerivWithinAt_eq_zero (h : IsMaxOn f s a) (hd : HasLineDerivWithinAt ℝ f f' s a b)
    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
  h.isExtr.hasLineDerivWithinAt_eq_zero hd h'

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