English
If hc is a differentiableWithinAt of c at x and hu is differentiableWithinAt of u at x, then the derivative within s of (c y)(u y) equals c' (u x) + c x (u' x).
Русский
Если c и u дифференцируемы внутри s в точке x, то производная внутри s от (c(y))(u(y)) равна c'(u(x)) + c(x)u'(x).
LaTeX
$$$\\text{differentiableWithinAt}(c,c',s,x) \\Rightarrow \\text{differentiableWithinAt}(y\\mapsto c(y)(u(y)),\\;s,x)$ и детерминированная формула$$
Lean4
theorem clm_apply (hc : HasStrictDerivAt c c' x) (hu : HasStrictDerivAt u u' x) :
HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + c x u') x :=
by
have := (hc.hasStrictFDerivAt.clm_apply hu.hasStrictFDerivAt).hasStrictDerivAt
rwa [add_apply, comp_apply, flip_apply, smulRight_apply, smulRight_apply, one_apply, one_smul, one_smul,
add_comm] at this
