English
If c and f are differentiable on a set s, then the function y ↦ c(y)·f(y) is differentiable on s.
Русский
Если c и f дифференцируемы на множестве s, то функция y ↦ c(y)·f(y) дифференцируема на s.
LaTeX
$$$$ \\text{DifferentiableOn } 𝕜 c s \\rightarrow \\text{DifferentiableOn } 𝕜 f s \\rightarrow \\text{DifferentiableOn } 𝕜 (fun y => c y · f y) s $$$$
Lean4
@[simp, fun_prop]
theorem fun_smul (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
DifferentiableAt 𝕜 (fun y => c y • f y) x :=
(hc.hasFDerivAt.smul hf.hasFDerivAt).differentiableAt