hasFPowerSeriesOnBall_pi_iff — Mathlib

English

Pi-power-series onBall is equivalent to the componentwise hasFPowerSeriesOnBall.

Русский

Pi-представление на шаре эквивалентно компонентному hasFPowerSeriesOnBall.

LaTeX

$$$\\text{hasFPowerSeriesOnBall_pi_iff} : (HasFPowerSeriesOnBall (fun x \\mapsto (f · x)) (pi p) e r) \\Leftrightarrow (\\forall i, HasFPowerSeriesOnBall (f i) (p i) e r)$$$

Lean4

theorem hasFPowerSeriesOnBall_pi_iff (hr : 0 < r) :
    HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r ↔
      ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r :=
  by
  simp_rw [← hasFPowerSeriesWithinOnBall_univ]
  exact hasFPowerSeriesWithinOnBall_pi_iff hr

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