iteratedDeriv_of_isOpen — Mathlib

English

If f and g are equal on an open set s, then their nth iterated derivatives are equal on s.

Русский

Если f и g равны на открытом множестве s, то их n-я повторная производная совпадает на s.

LaTeX

$$Set.EqOn (iteratedDeriv n f) (iteratedDeriv n g) s$$

Lean4

theorem iteratedDeriv_of_isOpen (hfg : Set.EqOn f g s) (hs : IsOpen s) (n : ℕ) :
    Set.EqOn (iteratedDeriv n f) (iteratedDeriv n g) s :=
  by
  refine fun x hx ↦ Filter.EventuallyEq.iteratedDeriv_eq n ?_
  filter_upwards [IsOpen.mem_nhds hs hx] with a ha
  exact hfg ha

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