mul — Mathlib

English

If hc and hd are HasDerivWithinAt for c and d, then HasDerivWithinAt for instHMul.hMul c d is given by the sum of two terms: c' d(x) and c(x) d'.

Русский

Если c и d имеют производную внутри s в x, то производная внутри s от произведения c(y) d(y) выражается суммой c'(x) d(x) и c(x) d'(x).

LaTeX

$$$\text{HasDerivWithinAt} \bigl( \lambda y, c(y) \cdot d(y) \bigr) s x \\equiv c'(x) d(x) + c(x) d'(x)$$$

Lean4

theorem mul (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) :
    HasDerivWithinAt (c * d) (c' * d x + c x * d') s x :=
  hc.fun_mul hd

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