summable_of_tendsto_order_atTop_nhds_top

English

If the order of a family of mv power series tends to infinity, then the family is summable.

Русский

Если порядок семейства mv-рядов стремится к бесконечности, то семейство суммируемо.

LaTeX

$$Tendsto (λ i, (f i).order) atTop (nhds TopENat.top) → Summable f$$

Lean4

/-- A family of `MvPowerSeries` is summable if their order tends to infinity. -/
theorem summable_of_tendsto_order_atTop_nhds_top (h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)) : Summable f :=
  summable_of_tendsto_weightedOrder_atTop_nhds_top h

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