English
If hc and hd are HasStrictDerivAt for c and d, then the derivative at x of the product c(y) d(y) is c' d(x) + c(x) d'.
Русский
Если c и d имеют строгую производную в x, то производная произведения c(y) d(y) в x равна c'(x) d(x) + c(x) d'(x).
LaTeX
$$$\operatorname{HasStrictDerivAt} (y \mapsto c(y) d(y)) x = c'(x) d(x) + c(x) d'(x)$$$
Lean4
theorem fun_mul (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) :
HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') x :=
by
have := (HasStrictFDerivAt.mul' hc hd).hasStrictDerivAt
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
