fun_smul — Mathlib

English

If UniqueDiffWithinAt 𝕜 s x holds, and c, f are differentiable within s at x, then fderivWithin of c·f equals c x · fderivWithin f + (fderivWithin c).smulRight (f x).

Русский

Если существует уникальная внутренняя разность в s в точке x и c, f дифференцируемы внутри s, то fderivWithin(c·f) равна c(x)·fderivWithin(f) + (fderivWithin(c)).smulRight(f(x)).

LaTeX

$$$$ \\text{fderivWithin 𝕜 (fun y => c y · f y) } s x = c x \\cdot fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x) $$$$

Lean4

@[simp, fun_prop]
theorem fun_smul (hc : Differentiable 𝕜 c) (hf : Differentiable 𝕜 f) : Differentiable 𝕜 fun y => c y • f y := fun x =>
  (hc x).smul (hf x)

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