English
If hc and hd are HasDerivWithinAt for c and d, then HasDerivWithinAt for their product is given by the standard product rule formula involving c, d, c', d'.
Русский
Если hc и hd задают производные внутри множества для функций c и d, то для их произведения выполняется обычное правило произведения, где участвуют c, d, c', d'.
LaTeX
$$$\text{HasDerivWithinAt}(c \cdot d)\; s\; x \\Rightarrow \\text{derivative} = c' d(x) + c(x) d'$, но в общем виде формула представлена как в оригинале.$$
Lean4
theorem fun_mul (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) :
HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') s x :=
by
have := (HasFDerivWithinAt.mul' hc hd).hasDerivWithinAt
rwa [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, one_smul,
one_smul, add_comm] at this
