proposition: Lemma acc_pt_bds_seq_ub : ∀ (a : ℕ → ℝ) (i : has_ub a) (x : ℝ), is_seq_acc_pt a x ⇒ ∀ m : ℕ, x ≤ sequence_ub a (i) m.
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). 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)) (iii). Because (iii) both (is_index_seq n) and (Un_cv (fun k ↦ a(n(k)), x)) hold. Take m : ℕ. Define L := (sequence_ub a (i) m). We argue by contradiction. Assume that (~ x <= L). It holds that (L < x). Define ε := (x - L). It holds that (ε > 0). It holds that (∃ K : ℕ, ∀ k : ℕ, (k ≥ K)%nat ⇒ R_dist (a (n k)) x < ε). Obtain such a K. Define Nn := (Nat.max K m). It holds that (R_dist (a (n Nn)) x < ε). By Rabs_def2 it holds that (a (n Nn) - x < ε ∧ - ε < a (n Nn) - x) (v). Because (v) both (a (n Nn) - x < ε) and (- ε < a (n Nn) - x) hold. It holds that (x - a (n Nn) < x - L). It holds that (a (n Nn) > L). By index_seq_grows_0 it holds that (n Nn ≥ Nn)%nat. By sequence_ub_bds it holds that (a (n Nn) ≤ L). Contradiction. Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type Automation Libs.Analysis.Sequences Libs.Analysis.Subsequences Libs.Analysis.SupAndInf Libs.Analysis.SequentialAccumulationPoints Notations Tactics