fun_const_smul — Mathlib

English

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

Русский

Если f и c дифференцируемы внутри 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

nonrec theorem fun_const_smul (c : R) (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (fun y => c • f y) (c • f') s x :=
  hf.const_smul c

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