hasLineDerivAt — Mathlib

English

If a line-derivative exists within s at x in direction v, and s contains x, then the line derivative exists at x in the same direction.

Русский

Если существует линейная производная внутри s в точке x по направлению v и x ∈ s, то линейная производная существует в точке x по направлению v.

LaTeX

$$$\text{HasLineDerivWithinAt}_{\mathbb{k}}(f,f',s,x,v) \land x \in s \Rightarrow \text{HasLineDerivAt}_{\mathbb{k}}(f,f',x,v)$$$

Lean4

theorem hasLineDerivAt (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : s ∈ 𝓝 x) : HasLineDerivAt 𝕜 f f' x v :=
  h.hasLineDerivAt' <| (Continuous.tendsto' (by fun_prop) 0 _ (by simp)).eventually hs

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