English
If ha: HasStrictFDerivAt a a' x and hb: HasStrictFDerivAt b b' x, then HasStrictFDerivAt (y ↦ a(y) · b(y)) (a x · b' + a' ⟪ b x) at x.
Русский
Если ha: HasStrictFDerivAt a a' x и hb: HasStrictFDerivAt b b' x, тогда HasStrictFDerivAt (y ↦ a(y) · b(y)) (a x · b' + a' ⟪ b x) в x.
LaTeX
$$$\text{HasStrictFDerivAt}\ a\ a'\ x \rightarrow \text{HasStrictFDerivAt}\ b\ b'\ x \rightarrow \text{HasStrictFDerivAt}\ (\\lambda y. a(y) \\cdot b(y))\ (a x \\cdot b' + a' \\langle\\cdot\\rangle b x)\ x$$$
Lean4
@[fun_prop]
theorem fun_mul' {x : E} (ha : HasStrictFDerivAt a a' x) (hb : HasStrictFDerivAt b b' x) :
HasStrictFDerivAt (fun y => a y * b y) (a x • b' + a' <• b x) x :=
((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasStrictFDerivAt (a x, b x)).comp x (ha.prodMk hb)
