fun_smul — Mathlib

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

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