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