proposition: Lemma seq_bdd_seq_acc_pts_bdd : ∀ a : ℕ → ℝ, has_ub a ⇒ bound (is_seq_acc_pt a).
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). We need to show that (there exists m : ℝ, is_upper_bound (is_seq_acc_pt a) m). We need to show that (there exists m : ℝ, for all x : ℝ, is_seq_acc_pt a x ⇨ x ≤ m). By (i) it holds that (there exists M : R, is_upper_bound (EUn a) M). Obtain such an M. It holds that (is_upper_bound (EUn a) M). Choose m := M. Take x : ℝ. Assume that (is_seq_acc_pt a x). It holds that (there exists n : ℕ ⇨ ℕ, is_index_seq n ∧ Un_cv (fun k ↦ a(n(k)), x)). Obtain such an n. It holds that (is_index_seq n ∧ Un_cv (fun k ↦ a(n(k)), x)) (iv). Because (iv) both (is_index_seq n) and (Un_cv (fun k ↦ (a(n(k))), x)) hold. We need to show that (x ≤ M). By (upp_bd_seq_is_upp_bd_lim (fun k => a (n k))) it suffices to show that (for all k : nat, (a (n k) <= M)). We claim that (for all k : ℕ, (a k) ≤ M) (v). { It holds that (for all x0 : ℝ, EUn a x0 ⇨ x0 ≤ M). It holds that (for all x0 : ℝ, (there exists k : ℕ, x0 = a k) ⇨ x0 ≤ M). Take k : ℕ. It suffices to show that (there exists k0 : nat, a k = a k0). Choose k0 := k. We conclude that (a k = a k0). } Take n0 : ℕ. By (v) it holds that (a(n n0) ≤ M). It follows that (a(n n0) ≤ M). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Analysis.Sequences Libs.Analysis.Subsequences Notations Tactics