hasLineDerivAt' — Mathlib

English

If s and t are eventually equal in nhds at x through a canonical line map, then HasLineDerivWithinAt with s is equivalent to that with t.

Русский

Если множества s и t эквивалентны почти во всём вокруг точки x по канонической карте линии, тогда HasLineDerivWithinAt для s эквивалентно HasLineDerivWithinAt для t.

LaTeX

$$$s =_\mathcal{N} x t \Rightarrow HasLineDerivWithinAt_{\mathbb{k}}(f,f',s,x,v) \iff HasLineDerivWithinAt_{\mathbb{k}}(f,f',t,x,v)$$$

Lean4

theorem hasLineDerivAt' (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : ∀ᶠ t : 𝕜 in 𝓝 0, x + t • v ∈ s) :
    HasLineDerivAt 𝕜 f f' x v :=
  h.hasDerivAt hs

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