comp_semilinear₁ — 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: F \toSL[σ] F' \text{ is } σ\text{-semilinear, then } L \circ f \circ σ' \text{ is differentiable at } σ x.$$$

Lean4

/-- If `f` is differentiable at `x`, and `L` is `σ`-semilinear, then `L ∘ f ∘ σ⁻¹` is
differentiable at `σ x`. -/
theorem comp_semilinear₁ (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (L ∘ f ∘ σ') (σ x) :=
  (hf.hasDerivAt.comp_semilinear σ' L).differentiableAt

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