fun_smul — Mathlib

English

If c and f are differentiable within s at x, then the product y ↦ c(y)·f(y) is differentiable within s at x.

Русский

Если c и f дифференцируемы внутри множества s в точке x, то произведение $c(y)·f(y)$ дифференцируемо внутри s в x.

LaTeX

$$$$ \\DifferentiableWithinAt 𝕜 c s x \\rightarrow \\DifferentiableWithinAt 𝕜 f s x \\rightarrow \\DifferentiableWithinAt 𝕜 (fun y => c y · f y) s x $$$$

Lean4

@[fun_prop]
theorem fun_smul (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :
    DifferentiableWithinAt 𝕜 (fun y => c y • f y) s x :=
  (hc.hasFDerivWithinAt.smul hf.hasFDerivWithinAt).differentiableWithinAt

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