lineDifferentiableWithinAt_iff_of_mem

English

If f0 and f1 agree on nhdsWithin x s, and x ∈ s, then line differentiability within s transfers from f to f1 along x in v.

Русский

Если f0 и f1 совпадают в nhdsWithin x s и x ∈ s, тогда линейная дифференцируемость внутри s переносится между f и f1.

LaTeX

$$$((nhdsWithin x s).EventuallyEq f_{0} f_{1}) \\land x \\in s \\Rightarrow \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{0},s;x,v) \\Rightarrow \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f_{1},s;x,v)$$$

Lean4

theorem lineDifferentiableWithinAt_iff_of_mem (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : x ∈ s) :
    LineDifferentiableWithinAt 𝕜 f₀ s x v ↔ LineDifferentiableWithinAt 𝕜 f₁ s x v :=
  h.lineDifferentiableWithinAt_iff (h.eq_of_nhdsWithin hx)

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