smul — Mathlib

English

If c and f are differentiable on s, then the map 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

@[fun_prop]
theorem smul (hc : DifferentiableOn 𝕜 c s) (hf : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (c • f) s := fun x hx =>
  (hc x hx).smul (hf x hx)

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