hasFDerivWithinAt_iff_of_mem — Mathlib

English

If f0 and f1 are eventually equal on nhds inside s around x, and x ∈ s, then HasFDerivWithinAt f0 f' s x iff HasFDerivWithinAt f1 f' s x.

Русский

Если f0 и f1 согласованы в окрестности x внутри s и x ∈ s, тогда HasFDerivWithinAt f0 f' s x эквивален HasFDerivWithinAt f1 f' s x.

LaTeX

$$$ \\mathrm{nhdsWithin}(x,s).\\text{EventuallyEq}(f_0,f_1) \\Rightarrow \\mathrm{HasFDerivWithinAt}(f_0,f',s,x) \\iff \\mathrm{HasFDerivWithinAt}(f_1,f',s,x) $$$

Lean4

theorem hasFDerivWithinAt_iff_of_mem (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : x ∈ s) :
    HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x :=
  h.hasFDerivWithinAt_iff (h.eq_of_nhdsWithin hx)

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