deriv_fun_smul — Mathlib

English

Let c: X → 𝕜 and f: X → F be differentiable at x with derivatives c'(x) and f'(x). Then the derivative at x of the map y ↦ c(y) f(y) is c(x) f'(x) + c'(x) f(x).

Русский

Пусть c: X → 𝕜 и f: X → F дифференцируемы в x с производными c'(x) и f'(x). Тогда производная в x от y ↦ c(y) f(y) равна c(x) f'(x) + c'(x) f(x).

LaTeX

$$$\\dfrac{d}{dy}\\bigl(c(y)f(y)\\bigr)\\Big|_{y=x} = c(x)\\,f'(x) + c'(x)\\,f(x)$$$

Lean4

theorem deriv_fun_smul (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
    deriv (fun y => c y • f y) x = c x • deriv f x + deriv c x • f x :=
  (hc.hasDerivAt.smul hf.hasDerivAt).deriv

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