English
If HasFPowerSeriesWithinOnBall f pf s (u x) r then HasFPowerSeriesWithinOnBall (f ∘ u) (pf.compContinuousLinearMap u) (Set.preimage (ContinuousLinearMap.funLike.coe u) s) x (r / ‖u‖ₑ).
Русский
Если существует разложение ряда в шаре для f вокруг u x, то для композиции f ∘ u существует разложение вокруг x с радиусом р/‖u‖.
LaTeX
$$HasFPowerSeriesWithinOnBall f pf s (ContinuousLinearMap.funLike.coe u x) r → HasFPowerSeriesWithinOnBall (Function.comp f (ContinuousLinearMap.funLike.coe u)) (pf.compContinuousLinearMap u) (Set.preimage (ContinuousLinearMap.funLike.coe u) s) x (instHDiv.hDiv r (SeminormedAddGroup.toContinuousENorm.enorm u))$$
Lean4
theorem compContinuousLinearMap (hf : AnalyticAt 𝕜 f (u x)) : AnalyticAt 𝕜 (f ∘ u) x :=
let ⟨p, hp⟩ := hf
⟨p.compContinuousLinearMap u, hp.compContinuousLinearMap⟩
