iteratedDerivWithin_congr — Mathlib

English

If two functions agree on a set s, then their nth iterated derivatives within s agree on s as well.

Русский

Если две функции совпадают на множестве s, то их n-ая повторная производная внутри s также совпадает на s.

LaTeX

$$$\\operatorname{EqOn} (\\operatorname{iteratedDerivWithin} n f s) (\\operatorname{iteratedDerivWithin} n g s) s$$

Lean4

theorem iteratedDerivWithin_congr (hfg : Set.EqOn f g s) :
    Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s := by
  induction n generalizing f g with
  | zero => rwa [iteratedDerivWithin_zero]
  | succ n IH =>
    intro y hy
    rw [iteratedDerivWithin_succ, iteratedDerivWithin_succ]
    exact derivWithin_congr (IH hfg) (IH hfg hy)

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