scomp_of_eq — Mathlib

English

If f is differentiable at x and σ, σ' are mutually inverse normed-ring automorphisms, then σ ∘ f ∘ σ' is differentiable at σ x with derivative σ f'.

Русский

Если f дифференцируема в x и σ, σ' взаимно обратны и являются нормированными автоморфизмами колец, то σ ∘ f ∘ σ' дифференцируема в σx с производной σ f'.

LaTeX

$$$\text{If } f \text{ is differentiable at } x \text{ and } σ, σ' \text{ are inverse normed-ring automorphisms, then } σ \circ f \circ σ' \text{ is differentiable at } σ x \text{ with derivative } σ f'.$$$

Lean4

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

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