iteratedDerivWithin_const_mul — Mathlib

English

If n > 0 and c is a scalar, then the nth iterated derivative within s of c · f equals c · the nth iterated derivative within s of f.

Русский

Если n > 0 и c — скаляр, то n-я повторная производная внутри s от c · f равна c · n-й повторной производной внутри s от f.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (c \\cdot f) s x = c \\cdot \\operatorname{iteratedDerivWithin}_n f s x$$$

Lean4

theorem iteratedDerivWithin_const_mul (c : 𝕜) {f : 𝕜 → 𝕜} (hf : ContDiffWithinAt 𝕜 n f s x) :
    iteratedDerivWithin n (fun z => c * f z) s x = c * iteratedDerivWithin n f s x := by
  simpa using iteratedDerivWithin_const_smul (F := 𝕜) hx h c hf

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