iteratedDerivWithin_const_sub — Mathlib

English

For 0 < n, the nth iterated derivative within s of c − f z equals the nth iterated derivative within s of −f z.

Русский

Для 0 < n n-я повторная производная внутри s от c − f z равна n-й повторной производной внутри s от −f z.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (\\lambda z. c - f z) s x = \\operatorname{iteratedDerivWithin}_n (\\lambda z. -f z) s x$$

Lean4

theorem iteratedDerivWithin_const_sub (hn : 0 < n) (c : F) :
    iteratedDerivWithin n (fun z => c - f z) s x = iteratedDerivWithin n (fun z => -f z) s x :=
  by
  obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'
  rw [iteratedDerivWithin_succ', iteratedDerivWithin_succ']
  congr 1 with y
  rw [derivWithin.fun_neg]
  exact derivWithin_const_sub _

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