comp_semilinear₂ — Mathlib

English

If f is differentiable at R z, then L ∘ f ∘ R is differentiable at z; this follows from the previous statement via simplification.

Русский

Если f дифференцируема в R z, то L ∘ f ∘ R дифференцируема в z; вывод следует из предыдущего утверждения.

LaTeX

$$$\mathrm{DifferentiableAt}_{\mathbb{K}} f (R z) \Rightarrow \mathrm{DifferentiableAt}_{\mathbb{K}} (L \circ f \circ R) z$$$

Lean4

/-- If `L` and `R` are semilinear maps whose composite is linear, and `f` is differentiable at
`R z`, then `L ∘ f ∘ R` is differentiable at `z`. -/
theorem comp_semilinear₂ {f : V → W} {z : V'} (hf : DifferentiableAt 𝕜 f (R z)) : DifferentiableAt 𝕜 (L ∘ f ∘ R) z := by
  simpa using (hf.hasFDerivAt.comp_semilinear L R).differentiableAt

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