hasDerivAt_of_bilinear — Mathlib

English

For a bilinear map B, the derivative of the map y ↦ B(u(y), v(y)) at y equals B(u(y), v'(y)) + B(u'(y), v(y)).

Русский

Для билинейной карты B производная по y функторной формы равна B(u(y), v'(y)) + B(u'(y), v(y)).

LaTeX

$$$\frac{d}{dy} B(u(y), v(y)) = B(u(y), v'(y)) + B(u'(y), v(y))$$$

Lean4

theorem hasDerivAt_of_bilinear (hu : HasDerivAt u u' x) (hv : HasDerivAt v v' x) :
    HasDerivAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) x := by
  simpa using (B.hasFDerivAt_of_bilinear hu.hasFDerivAt hv.hasFDerivAt).hasDerivAt

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