smul — Mathlib

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

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