fderivWithin_fun_smul — Mathlib

English

The derivative of the product c·f is f_{ξ} = c x · fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x).

Русский

Производная произведения c·f равна c(x)·f'(x) + f'(x)·(f(x)).

LaTeX

$$$$ \\text{fderiv } 𝕜 (c · f) x = c x · fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x) $$$$

Lean4

theorem fderivWithin_fun_smul (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
    (hf : DifferentiableWithinAt 𝕜 f s x) :
    fderivWithin 𝕜 (fun y => c y • f y) s x = c x • fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x) :=
  (hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).fderivWithin hxs

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