English
HasFPowerSeriesWithinAt for the product is equivalent to HasFPowerSeriesWithinAt for each component.
Русский
HasFPowerSeriesWithinAt по продукту эквивалентен HasFPowerSeriesWithinAt для каждой компоненты.
LaTeX
$$$HasFPowerSeriesWithinAt (fun x \\mapsto (f · x)) (FormalMultilinearSeries.pi p) s e \\Leftrightarrow \\forall i, HasFPowerSeriesWithinAt (f i) (p i) s e$$$
Lean4
theorem pi (hf : ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e) :
HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e :=
by
have : ∀ᶠ r in 𝓝[>] 0, ∀ i, HasFPowerSeriesWithinOnBall (f i) (p i) s e r :=
eventually_all.mpr (fun i ↦ (hf i).eventually)
obtain ⟨r, hr, r_pos⟩ := (this.and self_mem_nhdsWithin).exists
exact ⟨r, HasFPowerSeriesWithinOnBall.pi hr r_pos⟩
