derivWithin_smul — Mathlib

English

If c and f are differentiable within s at x, then derivWithin (c · f) s x = c(x) derivWithin f s x + derivWithin c s x · f(x).

Русский

Если c и f дифференцируемы внутри s в x, то derivWithin (c · f) s x = c(x) derivWithin f s x + derivWithin c s x · f(x).

LaTeX

$$$\\operatorname{derivWithin}_s\\bigl(c(y)f(y)\\bigr)(x) = c(x)\\operatorname{derivWithin}_s f(x) + \\operatorname{derivWithin}_s c(x)\\,f(x)$$$

Lean4

theorem derivWithin_smul (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :
    derivWithin (c • f) s x = c x • derivWithin f s x + derivWithin c s x • f x :=
  derivWithin_fun_smul hc hf

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