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