English
If two functions have formal power series expansions within sets, then their composition has a formal power series with the composed coefficients; i.e., HasFPowerSeriesWithinAt.comp.
Русский
Если две функции имеют разложения степенных рядов в рамках множеств, то их композиция имеет разложение степенного ряда с составленными коэффициентами.
LaTeX
$$$\\text{HasFPowerSeriesWithinAt}\\; g\\; q\\; t\\; (f x)\\; \\to\\; HasFPowerSeriesWithinAt\\; (g\\circ f)\\; (q\\circ p)\\; x$.$$
Lean4
/-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, within
two sets `s` and `t` such that `f` maps `s` to `t`, then `g ∘ f` is analytic at `x` within `s`. -/
theorem comp {g : F → G} {f : E → F} {x : E} {t : Set F} {s : Set E} (hg : AnalyticWithinAt 𝕜 g t (f x))
(hf : AnalyticWithinAt 𝕜 f s x) (h : Set.MapsTo f s t) : AnalyticWithinAt 𝕜 (g ∘ f) s x :=
by
let ⟨_q, hq⟩ := hg
let ⟨_p, hp⟩ := hf
exact (hq.comp hp h).analyticWithinAt
