isBounded_range_of_tendsto — Mathlib

English

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

Русский

Если последовательность u: ℕ → α сходится к x, то её образ ограничен.

LaTeX

$$$\\forall u: \\\\mathbb{N} \\to \\\\alpha, \\\\forall x:\\\\alpha, \\\\ Tendsto\\, u\\, atTop\\, (\\\\nhds x) \\Rightarrow \\\\ IsBounded(\\\\range u).$$$

Lean4

theorem isBounded_range_of_tendsto (u : ℕ → α) {x : α} (hu : Tendsto u atTop (𝓝 x)) : IsBounded (range u) :=
  hu.cauchySeq.isBounded_range

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