smul — Mathlib

English

Under UniqueDiffWithinAt, and differentiability of c and f within s, the fderivWithin of c·f equals c x · fderivWithin f + (fderivWithin c).smulRight (f x).

Русский

При UniqueDiffWithinAt и дифференцируемости внутри s, fderivWithin от c·f равна c(x)·fderivWithin f + (fderivWithin c).smulRight (f(x)).

LaTeX

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

Lean4

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

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