scomp — Mathlib

English

If f has strict Frechet derivative f' at x and h is σ-semi-linear, then σ ∘ f ∘ σ' has strict derivative σ f' at σ x.

Русский

Если f имеет строгую производную f' в x и h является σ-симилинейным, то σ ∘ f ∘ σ' имеет строгую производную σ f' в σx.

LaTeX

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

Lean4

theorem scomp (hg : HasStrictDerivAt g₁ g₁' (h x)) (hh : HasStrictDerivAt h h' x) :
    HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x := by simpa using ((hg.restrictScalars 𝕜).comp x hh).hasStrictDerivAt

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