iteratedFDerivWithin_eventually_congr_set'

English

If two sets agree on nhds x, their iterated derivatives at x coincide for all orders.

Русский

Если множества совпадают в окрестности x, то их итеративные производные в x совпадают для всех порядков.

LaTeX

$$$\forall h: (nhds x).EventuallyEq s t,\forall n, iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x$$$

Lean4

theorem iteratedFDerivWithin_eventually_congr_set' (y : E) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t := by
  induction n generalizing x with
  | zero => rfl
  | succ n ihn =>
    refine (eventually_nhds_nhdsWithin.2 h).mono fun y hy => ?_
    simp only [iteratedFDerivWithin_succ_eq_comp_left, (· ∘ ·)]
    rw [(ihn hy).fderivWithin_eq_of_nhds, fderivWithin_congr_set' _ hy]

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