fun_const_smul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

nonrec theorem fun_const_smul (c : R) (hf : HasDerivAt f f' x) : HasDerivAt (fun y => c • f y) (c • f') x :=
  hf.const_smul c

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