const_smul — Mathlib

English

Within a set s, the derivative of y ↦ c(y) f(y) at x equals c(x) derivWithin f s x + derivWithin c s x · f(x), under differentiability assumptions.

Русский

Внутри множества s производная y ↦ c(y) f(y) в 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 const_smul (c : R) (hf : HasDerivWithinAt f f' s x) : HasDerivWithinAt (c • f) (c • f') s x :=
  hf.const_smul c

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