comp_analyticOn — Mathlib

English

If g is linear and f is analytic on s in the nhd sense, then g ∘ f is analytic on s in the nhd sense.

Русский

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

LaTeX

$$$\text{AnalyticOnNhd}_{\mathcal{K}}(f,s) \Rightarrow \text{AnalyticOnNhd}_{\mathcal{K}}(g\circ f,s)$$$

Lean4

/-- If a function `f` is analytic on a set `s` and `g` is linear, then `g ∘ f` is analytic
on `s`. -/
theorem comp_analyticOn (g : F →L[𝕜] G) (h : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (g ∘ f) s :=
  by
  rintro x hx
  rcases h x hx with ⟨p, r, hp⟩
  exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesWithinOnBall hp⟩

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