fun_smul — Mathlib

English

If c and f are differentiable on a set s, then the product function is differentiable on s.

Русский

Если c и f дифференцируемы на множестве s, то произведение – дифференцируемо на 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 fun_smul (hc : DifferentiableOn 𝕜 c s) (hf : DifferentiableOn 𝕜 f s) :
    DifferentiableOn 𝕜 (fun y => c y • f y) s := fun x hx => (hc x hx).smul (hf x hx)

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