Unbounded_Monotone_Sequence_Diverges_to_Infinity

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

limits-of-sequencesproofwikiunbounded-monotone-sequence-diverges-to-infinity

Let $\sequence {x_n}$ be a sequence in $\R$ . Let $\sequence {x_n}$ be monotone, that is either increasing or decreasing.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic

theorem Unbounded_Monotone_Sequence_Diverges_to_Infinity (x : ℕ → ℝ) (hm : Monotone x) (hub : ¬BddAbove (Set.range x)) : Filter.Tendsto x Filter.atTop Filter.atTop := by sorry

Source

https://proofwiki.org/wiki/Unbounded_Monotone_Sequence_Diverges_to_Infinity

View graph