Divergent_Sequence_may_be_Bounded
Provedlimits-of-sequencesproofwiki
There exists a bounded sequence that does not converge.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Divergent_Sequence_may_be_Bounded : ∃ x : ℕ → ℝ, (¬ ∃ l, Filter.Tendsto x Filter.atTop (nhds l)) ∧ BddAbove (Set.range x) ∧ BddBelow (Set.range x) := by sorry
Source