comp_hasFPowerSeriesOnBall — Mathlib

English

If g is linear and h is analytic on s, then g ∘ f is analytic on s.

Русский

Если g линейна и f аналитична на s, то g ∘ f аналитична на s.

LaTeX

$$$\text{AnalyticOn}_{\mathcal{K}}(f,s) \Rightarrow \text{AnalyticOn}_{\mathcal{K}}(g\circ f,s)$ (при линейности g)$$

Lean4

/-- If a function `f` has a power series `p` on a ball and `g` is linear, then `g ∘ f` has the
power series `g ∘ p` on the same ball. -/
theorem comp_hasFPowerSeriesOnBall (g : F →L[𝕜] G) (h : HasFPowerSeriesOnBall f p x r) :
    HasFPowerSeriesOnBall (g ∘ f) (g.compFormalMultilinearSeries p) x r :=
  by
  rw [← hasFPowerSeriesWithinOnBall_univ] at h ⊢
  exact g.comp_hasFPowerSeriesWithinOnBall h

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