Convergent sequences are bounded above

Stream: new members

[Harry Pacitti]

Hi there,

I'm trying to prove that convergent sequences are bounded above. I've included a proof that convergent sequences are eventually bounded above. I want to use the maximum of $s_1, s_2,....,s_{(N-1)}, a+1$.

import data.real.basic

def converges_to (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε

variables {s : ℕ → ℝ} {a : ℝ}

theorem exists_le_of_converges_to_ev (cs : converges_to s a) :
  ∃ N b, ∀ n, N ≤ n → s n < b :=
begin
cases cs 1 zero_lt_one with N h,
use [N , a + 1],
intros n h₁,
specialize @h n h₁,
have h₂: s n - a ≤ abs(s n - a),
apply le_abs_self,
suffices h₃: s n - a < 1,
exact sub_lt_iff_lt_add'.mp h₃,
apply lt_of_le_of_lt h₂ h,
end

theorem exists_le_of_converges_to_eventually (cs : converges_to s a) :
  ∃ b, ∀ n, s n < b :=
begin
cases cs 1 zero_lt_one with N h,
sorry
end

[Filippo A. E. Nuccio]

Can you produce a mwe?

[Harry Pacitti]

That should work now.