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