iteratedDerivWithin_const_add — Mathlib

English

If n > 0 and c is a constant, then the nth iterated derivative within s of the function z ↦ c + f z equals the nth iterated derivative of f within s at x.

Русский

Если n > 0 и константа c, то n-я повторная производная внутри s функции z ↦ c + f(z) равна n-й повторной производной f внутри s в точке x.

LaTeX

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

Lean4

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

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