iteratedDerivWithin_neg — Mathlib

English

The nth iterated derivative within s of f − g equals the nth iterated derivative within s of f minus that of g.

Русский

n-я повторная производная внутри s от f − g равна разности повторных производных внутри s от f и g.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (f - g) s x = \\operatorname{iteratedDerivWithin}_n f s x - \\operatorname{iteratedDerivWithin}_n g s x$$

Lean4

theorem iteratedDerivWithin_neg : iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x := by
  induction n generalizing x with
  | zero => simp
  | succ n IH =>
    simp only [iteratedDerivWithin_succ]
    rw [← derivWithin.neg]
    congr with y
    exact IH

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