fderivWithin_smul — Mathlib

English

For differentiable c and f at x with respect to 𝕜, the fderiv of c·f equals c x · fderiv f x + (fderiv c x).smulRight (f x).

Русский

При differentiable c и f в точке x производная от c·f равна c(x)·fderiv f(x) + fderiv c(x)·(f(x)).

LaTeX

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

Lean4

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

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