English
If ha: HasFDerivWithinAt a a' s x and hb: HasFDerivWithinAt b b' s x, then HasFDerivWithinAt (y ↦ a(y) * b(y)) with derivative a x • b' + a' <• b x.
Русский
Если ha: HasFDerivWithinAt a a' s x и hb: HasFDerivWithinAt b b' s x, то HasFDerivWithinAt (y ↦ a(y) * b(y)) имеет производную a x • b' + a' <• b x.
LaTeX
$$$\text{HasFDerivWithinAt}\ a\ a'\ s\ x \rightarrow \text{HasFDerivWithinAt}\ b\ b'\ s\ x \rightarrow \text{HasFDerivWithinAt}\ (instHMul.hMul (a y) (b y))\ (a x \cdot b' + a' \cdot b x)\ s\ x$$$
Lean4
@[fun_prop]
theorem mul (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) : HasFDerivAt (c * d) (c x • d' + d x • c') x :=
hc.fun_mul hd
