pi — Mathlib · SciLib

English

The HasFPowerSeriesAt for all i implies HasFPowerSeriesAt for their pi-product.

Русский

HasFPowerSeriesAt для всех i подразумевает HasFPowerSeriesAt для их pi-произведения.

LaTeX

$$$HasFPowerSeriesAt (fun x \\mapsto (f i x)) (pi p) e \\Rightarrow (∀ i, HasFPowerSeriesAt (f i) (p i) e)$$$

Lean4

theorem pi (hf : ∀ i, HasFPowerSeriesAt (f i) (p i) e) :
    HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e :=
  by
  simp_rw [← hasFPowerSeriesWithinAt_univ] at hf ⊢
  exact HasFPowerSeriesWithinAt.pi hf

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