hasLineDerivWithinAt_iff_of_mem — Mathlib

English

If f0 and f1 are eventually equal on nhds within s at x, and x ∈ s, then HasLineDerivWithinAt equivalence holds.

Русский

Если f0 и f1 совпадают у x внутри s в nhds и x ∈ s, тогда эквивалентность линейной производной внутри сохраняется.

LaTeX

$$$(nhdsWithin x s).EventuallyEq f_{0} f_{1} \\land x \\in s \\Rightarrow \\mathrm{HasLineDerivWithinAt}_{\\mathbb{K}}(f_{0},f',s,x,v) \\iff \\mathrm{HasLineDerivWithinAt}_{\\mathbb{K}}(f_{1},f',s,x,v)$$$

Lean4

theorem hasLineDerivWithinAt_iff_of_mem (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : x ∈ s) :
    HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v :=
  h.hasLineDerivWithinAt_iff (h.eq_of_nhdsWithin hx)

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