multipliable_one_add_of_tendsto_order_atTop_nhds_top

English

If the order of f_i tends to infinity, then 1 + f_i is Multipliable.

Русский

Если порядок f_i стремится к бесконечности, то 1 + f_i множимо.

LaTeX

$$Multipliable (1 + f ·) via order$$

Lean4

/-- A family of `MvPowerSeries` in the form `1 + f i` is multipliable if the order of `f i`
tends to infinity. -/
theorem multipliable_one_add_of_tendsto_order_atTop_nhds_top (h : Tendsto (fun i ↦ (f i).order) atTop (nhds ⊤)) :
    Multipliable (1 + f ·) :=
  multipliable_one_add_of_summable_prod <| summable_prod_of_tendsto_order_atTop_nhds_top h

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