const_smul — Mathlib

English

A general form of the Leibniz-type rule inside a set: 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

nonrec theorem const_smul (c : R) (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (c • f) (c • f') x := by
  simpa using (hf.const_smul c).hasStrictDerivAt

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