scomp — Mathlib

English

If g₁ has strict derivative g₁' at h x and h has strict derivative h' at x, then g₁ ∘ h has strict derivative h' · g₁' at x.

Русский

Если у g₁ есть строгая производная g₁' в h x и у h строгая производная h' в x, то g₁ ∘ h имеет строгую производную h' · g₁' в x.

LaTeX

$$$\text{If } g_1 \text{ has strict derivative } g_1' \text{ at } h x \text{ and } h \text{ has strict derivative } h' \text{ at } x, \text{ then } (g_1 \circ h)'(x) = h' \cdot g_1'. $$$

Lean4

/-- The chain rule. -/
nonrec theorem scomp (hg : HasDerivAt g₁ g₁' (h x)) (hh : HasDerivAt h h' x) : HasDerivAt (g₁ ∘ h) (h' • g₁') x :=
  hg.scomp x hh hh.continuousAt

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