iteratedDerivWithin_const_smul — Mathlib

English

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

Русский

Если 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_smul (c : R) (hf : ContDiffWithinAt 𝕜 n f s x) :
    iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x :=
  by
  simp_rw [iteratedDerivWithin]
  rw [iteratedFDerivWithin_const_smul_apply hf h hx]
  simp only [ContinuousMultilinearMap.smul_apply]

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