pi — Mathlib · SciLib

English

The ball version of pi-power-series is equivalent to the univ version.

Русский

Эквивалентность шаровой версии pi-представления и версии на множестве.

LaTeX

$$$HasFPowerSeriesOnBall (fun x \\mapsto (f i x)) (pi p) e r \\Leftrightarrow HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (pi p) Set.univ e r$$$

Lean4

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

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