compContinuousLinearMap — Mathlib

English

If a HasFPowerSeriesWithinOnBall f pf s (u x) r holds, then HasFPowerSeriesWithinOnBall (f ∘ u) (pf.compContinuousLinearMap u) (u⁻¹' s) x (r / ‖u‖)

Русский

Если существует разложение в шаре для f вокруг u x, то для композиции f∘u существует разложение вокруг x с нормой u, радиус делится на ‖u‖.

LaTeX

$$HasFPowerSeriesWithinOnBall f pf s (ContinuousLinearMap.funLike.coe u x) r → HasFPowerSeriesWithinOnBall (f ∘ u) (pf.compContinuousLinearMap u) (Set.preimage (ContinuousLinearMap.funLike.coe u) s) x (r / ‖u‖ₑ)$$

Lean4

theorem compContinuousLinearMap (hf : HasFPowerSeriesOnBall f pf (u x) r) :
    HasFPowerSeriesOnBall (f ∘ u) (pf.compContinuousLinearMap u) x (r / ‖u‖ₑ) :=
  by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
  exact hf.compContinuousLinearMap

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