mul — Mathlib

English

If c and d have strict derivatives at x, then the product map y ↦ c(y) · d(y) has derivative (c x • d' + d x • c').

Русский

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

LaTeX

$$$\text{HasFDerivAt}\ c\ c'\ x \rightarrow \text{HasFDerivAt}\ d\ d'\ x \rightarrow \text{HasFDerivAt}\ (c(y) \cdot d(y))\ (c x \cdot d' + d x \cdot c')\ x$$$

Lean4

@[fun_prop]
theorem mul (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
    HasFDerivWithinAt (c * d) (c x • d' + d x • c') s x :=
  hc.fun_mul hd

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