mul — Mathlib

English

If hc and hd are HasStrictDerivAt for c and d, then the product rule for the product c(y) d(y) holds in the strict sense.

Русский

Если c и d имеют строгую производную, то правило произведения для их произведения выполняется в строгом смысле.

LaTeX

$$$\operatorname{HasStrictDerivAt}(c \cdot d) x = c'(x) d(x) + c(x) d'(x)$$$

Lean4

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

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