deriv_fun_mul — Mathlib

English

If c and d are differentiable at x, then the derivative of the product y ↦ c(y) d(y) is given by the sum of two products: c'(x) d(x) + c(x) d'(x).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem deriv_fun_mul (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    deriv (fun y => c y * d y) x = deriv c x * d x + c x * deriv d x :=
  (hc.hasDerivAt.mul hd.hasDerivAt).deriv

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