scomp_hasDerivAt_of_eq — Mathlib

English

If hg is HasDerivWithinAt g₁ g₁' y with hy: y = h x, and hh is HasDerivAt h h' x, then HasDerivWithinAt (g₁ ∘ h) (h' · g₁') s x.

Русский

Если hg имеет HasDerivWithinAt для g₁, g₁' в y с y = h x, и hh имеет HasDerivAt h h' x, тогда HasDerivWithinAt (g₁ ∘ h) (h' · g₁') s x.

LaTeX

$$$\text{If } hg : HasDerivWithinAt g_1 g_1' y \text{ with } hy: y = h x, \text{ and } hh : HasDerivAt h h' x, \text{ then } HasDerivWithinAt (g_1 \circ h) (h' \cdot g_1') s x.$$$

Lean4

theorem scomp_hasDerivAt_of_eq (hg : HasDerivWithinAt g₁ g₁' s' y) (hh : HasDerivAt h h' x) (hs : ∀ x, h x ∈ s')
    (hy : y = h x) : HasDerivAt (g₁ ∘ h) (h' • g₁') x := by rw [hy] at hg; exact hg.scomp_hasDerivAt x hh hs

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