scomp_of_eq — Mathlib

English

If y = h x and HasDerivAt g₁ g₁' y, HasDerivAt h h' x, then HasDerivAt (g₁ ∘ h) (h' · g₁') x.

Русский

Если y = h x и HasDerivAt g₁ g₁' y, HasDerivAt h h' x, тогда HasDerivAt (g₁ ∘ h) (h' · g₁') x.

LaTeX

$$$\text{If } y = h x \text{ and } \text{HasDerivAt } g_1\; g_1'\; y, \text{HasDerivAt } h\; h'\; x, \text{ then } \text{HasDerivAt } (g_1 \circ h) (h' \cdot g_1') x.$$$

Lean4

theorem scomp_of_eq (hg : HasDerivAtFilter g₁ g₁' y L') (hh : HasDerivAtFilter h h' x L) (hy : y = h x)
    (hL : Tendsto h L L') : HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L := by rw [hy] at hg; exact hg.scomp x hh hL

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