fun_smul — Mathlib

English

If c has derivative c' and f has derivative f' at x, then the product y ↦ c(y) f(y) has derivative c(x) f'(x) + c'(x) f(x) at x.

Русский

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

LaTeX

$$$\text{If } \text{HasDerivWithinAt } c\, c' \; s\; x \text{ and } \text{HasDerivWithinAt } f\, f' \; s\; x, \; \text{then } \text{HasDerivWithinAt } (c\cdot f)\ (c x f' + c' f x)\ s\ x.$$$

Lean4

theorem fun_smul (hc : HasDerivWithinAt c c' s x) (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) s x := by
  simpa using (HasFDerivWithinAt.smul hc hf).hasDerivWithinAt

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