hasFPowerSeriesWithinAt_pi_iff — Mathlib

English

HasFPowerSeriesWithinOnBall for pi implies HasFPowerSeriesWithinOnBall for each i.

Русский

HasFPowerSeriesWithinOnBall для pi означает HasFPowerSeriesWithinOnBall для каждого i.

LaTeX

$$$\\forall hr>0, HasFPowerSeriesWithinOnBall (fun x => (f · x)) (FormalMultilinearSeries.pi p) e r \\Leftrightarrow \\forall i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r$$$

Lean4

theorem hasFPowerSeriesWithinAt_pi_iff :
    HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e ↔
      ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e :=
  by
  refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
  obtain ⟨r, hr⟩ := h
  exact ⟨r, (hasFPowerSeriesWithinOnBall_pi_iff hr.r_pos).1 hr i⟩

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