English
If UniqueDiffWithinAt 𝕜 s x and c, f are differentiable within s, then fderivWithin of c·f equals c x · fderivWithin f s x + (fderivWithin 𝕜 c s x).smulRight (f x).
Русский
Если UniqueDiffWithinAt 𝕜 s x и c, f дифференцируемы внутри s, то fderivWithin(c·f) равна c x · fderivWithin f s x + (fderivWithin c s x).smulRight (f x).
LaTeX
$$$$ \\text{fderivWithin } 𝕜 (c · f) s x = c x · fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x) $$$$
Lean4
theorem fderiv_fun_smul (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
fderiv 𝕜 (fun y => c y • f y) x = c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x) :=
(hc.hasFDerivAt.smul hf.hasFDerivAt).fderiv
