scomp_of_eq — Mathlib

English

If f is differentiable at x and L is σ-semi-linear, then L ∘ f ∘ σ' is differentiable at σ x.

Русский

Если f дифференцируема в x и L - σ-симилинейно, то L ∘ f ∘ σ' дифференцируема в σx.

LaTeX

$$$\text{If } f \text{ is differentiable at } x, \text{ and } L \text{ is } σ\text{-semilinear, then } L \circ f \circ σ' \text{ is differentiable at } σ x.$$$

Lean4

/-- The chain rule. -/
theorem scomp_of_eq (hg : HasDerivAt g₁ g₁' y) (hh : HasDerivAt h h' x) (hy : y = h x) :
    HasDerivAt (g₁ ∘ h) (h' • g₁') x := by rw [hy] at hg; exact hg.scomp x hh

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