bddAbove_range_of_tendsto_atTop_atBot

English

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

Русский

Для любого конечного s, если каждое u_k ограничено сверху по f, то сумма по 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 bddAbove_range_of_tendsto_atTop_atBot [IsDirected α (· ≤ ·)] {u : ℕ → α} (hx : Tendsto u atTop atBot) :
    BddAbove (Set.range u) :=
  hx.isBoundedUnder_le_atBot.bddAbove_range

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