clm_comp — Mathlib

English

If hc is strict derivative of c at x and hu is strict derivative of u at x, then the derivative of y ↦ (c(y))(u(y)) is c'(u(x)) + c(x)(u'(x)).

Русский

Если c имеет строгую производную в x и u имеет строгую производную в x, то производная y ↦ c(y)(u(y)) равна c'(u(x)) + c(x)(u'(x)).

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_comp (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) :
    HasDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.clm_comp hd

Похожие утверждения