multipliable_one_add_of_tendsto_order_atTop_nhds_top

English

If the orders of f_i tend to infinity, then the family 1 + f_i is multipliable.

Русский

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

LaTeX

$$$ \\text{Multipliable } (1 + f \\cdot) $ given $\\text{tendsto order to } \\top$$$

Lean4

/-- A family of `PowerSeries` 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

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