fderivWithin_eq_of_insert — Mathlib

English

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

Русский

Если f1 равна f на nhdsWithin x (insert x s), то fderivWithin f1 s x = fderivWithin f s x.

LaTeX

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

Lean4

theorem fderivWithin_eq_of_insert (hs : f₁ =ᶠ[𝓝[insert x s] x] f) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
  by
  apply Filter.EventuallyEq.fderivWithin_eq (nhdsWithin_mono _ (subset_insert x s) hs)
  exact (mem_of_mem_nhdsWithin (mem_insert x s) hs :)

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