hasLineDerivWithinAt_eq_zero — Mathlib

English

Let IsMinOn f s a. If HasLineDerivWithinAt f f' s a b and a right-ward approach t → 0 stays in s, then the line derivative is zero.

Русский

Пусть IsMinOn f s a. Если существует линейная производная вдоль линии внутри s и вправо от a, и при этом a+t b ∈ s для бесконечно малых t>0, то линейная производная равна нулю.

LaTeX

$$$\text{IsMinOn}(f,s,a) \land \text{HasLineDerivWithinAt}(f,f',s,a,b) \land \forall^{\mathrm{frequent}} t:\ a+t b \in s \Rightarrow f' = 0$$$

Lean4

theorem hasLineDerivWithinAt_eq_zero (h : IsMinOn 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'

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