fderivWithin_eq_of_mem — Mathlib

English

If f1 equals f on nhdsWithin x s, then fderivWithin f1 s x = fderivWithin f s x.

Русский

Если f1 совпадает с f на nhdsWithin x s, то fderivWithin f1 s x равно fderivWithin f s x.

LaTeX

$$$ (nhdsWithin x s).\\text{EventuallyEq}(f_1,f) \\to \\mathrm{fderivWithin}(f_1,s,x) = \\mathrm{fderivWithin}(f,s,x) $$$

Lean4

theorem fderivWithin_eq_of_mem (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
  hs.fderivWithin_eq (mem_of_mem_nhdsWithin hx hs :)

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