comp_contDiffAt_iff — Mathlib

English

If f has a Taylor expansion and g is a linear map, then f ∘ g has a Taylor expansion whose kth term is the kth term of f composed with g.

Русский

Если f имеет разложение по Тейлору, а g – линейное отображение, то f ∘ g имеет ряд Тейлора, где k-й член равен коэффициенту f при композиции с g.

LaTeX

$$$\text{HasFTaylorSeriesUpToOn}_{n} f p s \Rightarrow \text{HasFTaylorSeriesUpToOn}_{n} (f\circ g) (g^{-1}'s) (x) $$$

Lean4

/-- Composition by continuous linear equivs on the left respects higher differentiability at a
point. -/
theorem comp_contDiffAt_iff (e : F ≃L[𝕜] G) : ContDiffAt 𝕜 n (e ∘ f) x ↔ ContDiffAt 𝕜 n f x := by
  simp only [← contDiffWithinAt_univ, e.comp_contDiffWithinAt_iff]

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