English
If hc is strict deriv of c at x and hu is strict deriv of u at x, then HasStrictDerivAt of y ↦ (c y)(u y) equals c'(u x) + c x u'.
Русский
Если c и u имеют строгие производные, то производная композиции равна c'(u x) + c(x)u'.
LaTeX
$$$HasStrictDerivAt\\left(c,c',x\\right) \\Rightarrow HasStrictDerivAt\\left(y \\mapsto (c(y))(u(y))\\right)\\left(c'(u(x)) + c(x)u'\\right) x$$$
Lean4
theorem clm_apply (hc : HasDerivWithinAt c c' s x) (hu : HasDerivWithinAt u u' s x) :
HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + c x u') s x :=
by
have := (hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).hasDerivWithinAt
rwa [add_apply, comp_apply, flip_apply, smulRight_apply, smulRight_apply, one_apply, one_smul, one_smul,
add_comm] at this
