fun_mul — Mathlib

English

If hc and hd are HasDerivAt for c and d, then the derivative at x of the product c(y) d(y) is c'(x) d(x) + c(x) d'(x).

Русский

Если c и d имеют производную в точке x, то производная произведения c(y) d(y) в x равна c'(x) d(x) + c(x) d'(x).

LaTeX

$$$\operatorname{deriv} (y \mapsto c(y) \cdot d(y)) x = c'(x) \cdot d(x) + c(x) \cdot d'(x)$$$

Lean4

theorem fun_mul (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) :
    HasDerivAt (fun y => c y * d y) (c' * d x + c x * d') x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.mul hd

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