fun_smul — Mathlib

English

Let c: X → 𝕜 and f: X → F be differentiable at a point x with derivatives c'(x) and f'(x). Then the derivative at x of the product y ↦ c(y) f(y) satisfies d/dy [c(y) f(y)]|_{y=x} = c(x) f'(x) + c'(x) f(x).

Русский

Пусть c: X → 𝕜 и f: X → F дифференцируемы в точке x с производными c'(x) и f'(x). Тогда производная по y в точке 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 fun_smul (hc : HasDerivAt c c' x) (hf : HasDerivAt f f' x) :
    HasDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.smul hf

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