English
If hc and hd are strict derivatives, then the derivative of the composition of the maps c(y) and d(y) is the sum of c'∘d(x) and c(x)∘d'.
Русский
Если c и d имеют строгие производные, то производная композиции c(y)∘d(y) равняется сумме c'(d(x)) и c(x)∘d'(x).
LaTeX
$$$HasStrictDerivAt\\left( c,c',x\\right) \\Rightarrow HasStrictDerivAt\\left( y \\mapsto (c(y)\\circ(d(y)))\\right)\\left(c'\\circ(d(x)) + c(x)\\circ d'\\right) x$$$
Lean4
theorem clm_comp (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) :
HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x :=
by
have := (hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).hasDerivWithinAt
rwa [add_apply, comp_apply, comp_apply, smulRight_apply, smulRight_apply, one_apply, one_smul, one_smul,
add_comm] at this
