fderivWithin_fderivWithin_eq_of_eventuallyEq

English

If two sets s,t agree eventually near x, then fderivWithin f s and fderivWithin f t coincide at x.

Русский

Если множества согласуются почти рядом с x, то их fderivWithin совпадают в x.

LaTeX

$$$s =^\\!\\!_{\\mathcal{N} x} t \\Rightarrow fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x$$$

Lean4

theorem fderivWithin_fderivWithin_eq_of_eventuallyEq (h : s =ᶠ[𝓝 x] t) :
    fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x :=
  calc
    fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x :=
      (fderivWithin_eventually_congr_set h).fderivWithin_eq_of_nhds
    _ = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x := fderivWithin_congr_set h

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