bddBelow_range — Mathlib

English

If a sequence u : ℕ → α converges to a along atTop, then its range is bounded below.

Русский

Если последовательность u: ℕ → α сходится к a вдоль atTop, то её множество значений ограничено снизу.

LaTeX

$$$ [IsDirected α (≥)] {u:\mathbb{N}\to α} (h: Tendsto\, u\, atTop\, (\mathcal{N}a)) \Rightarrow BddBelow (Set.range\, u). $$$

Lean4

theorem bddBelow_range [IsDirected α (· ≥ ·)] {u : ℕ → α} (h : Tendsto u atTop (𝓝 a)) : BddBelow (Set.range u) :=
  h.isBoundedUnder_ge.bddBelow_range

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