by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
limits-of-sequencesproofwiki
Let \sequencexn be a sequence in R. Let \sequencexn be bounded. Let the limit superior of \sequencexn be l. Let the limit inferior of \sequencexn be l. Then ∀ϵ>0:∃N:∀n>N:xn<l+ϵ∀ϵ>0:∃N:∀n>N:xn>l−ϵ
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Terms_of_Bounded_Sequence_Within_Bounds (x : ℕ → ℝ) (hb : BddAbove (Set.range x)) (hb2 : BddBelow (Set.range x)) : ∀ n, sInf (Set.range x) ≤ x n ∧ x n ≤ sSup (Set.range x) := by sorry