bddBelow_range_of_tendsto_atTop_atTop

English

For any finite s, if every u_k is f-bounded below, then the sum over s is f-bounded below.

Русский

Для любого конечного s, если каждый u_k ограничен снизу по ≥, сумма по k∈s тоже ограничена снизу.

LaTeX

$$$\forall s\, (\forall k\in s, f.IsBoundedUnder(≥)\ (u_k)) \Rightarrow f.IsBoundedUnder(≥)\left(\sum_{k \in s} u_k\right)$$$

Lean4

theorem bddBelow_range_of_tendsto_atTop_atTop [IsDirected α (· ≥ ·)] {u : ℕ → α} (hx : Tendsto u atTop atTop) :
    BddBelow (Set.range u) :=
  hx.isBoundedUnder_ge_atTop.bddBelow_range

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