English
If the weighted order of f_i tends to infinity, then the family 1 + f_i is Multipliable.
Русский
Если взвешенный порядок f_i стремится к бесконечности, то семейство 1 + f_i множимо.
LaTeX
$$Multipliable (1 + f ·)$$
Lean4
/-- A family of `MvPowerSeries` in the form `1 + f i` is multipliable if the weighted order of `f i`
tends to infinity. -/
theorem multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top {w : σ → ℕ}
(h : Tendsto (fun i ↦ weightedOrder w (f i)) atTop (nhds ⊤)) : Multipliable (1 + f ·) :=
multipliable_one_add_of_summable_prod <| summable_prod_of_tendsto_weightedOrder_atTop_nhds_top h
