derivWithin_mul — Mathlib

English

The within-version of the product rule for differentiable c and d gives the derivative within s as a sum of two product terms.

Русский

Версия внутри множества правила произведения для дифференцируемых c и d дает производную внутри s как сумму двух слагаемых-произведений.

LaTeX

$$$\operatorname{derivWithin}(c \cdot d) \, s \, x = (\operatorname{derivWithin} c \, s \, x) \cdot d(x) + c(x) \cdot (\operatorname{derivWithin} d \, s \, x)$$$

Lean4

theorem derivWithin_mul (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :
    derivWithin (c * d) s x = derivWithin c s x * d x + c x * derivWithin d s x :=
  derivWithin_fun_mul hc hd

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