scomp — Mathlib

English

If g₁ has derivative g₁' at h x and h has derivative h' at x, then the filtered derivative of g₁ ∘ h at x is h' · g₁'.

Русский

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

LaTeX

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

Lean4

theorem scomp (hg : HasDerivAtFilter g₁ g₁' (h x) L') (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
    HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L := by simpa using ((hg.restrictScalars 𝕜).comp x hh hL).hasDerivAtFilter

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