proposition: Theorem Bolzano_Weierstrass : ∀ (a : ℕ → ℝ), has_ub a ⇒ (has_lb a ⇒ ∃ (n : ℕ → ℕ) (l : ℝ), is_index_seq n ∧ Un_cv (fun (k : ℕ) ↦ a (n k)) l ).
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). Assume that (has_lb a) (ii). Define iii := (maj_min a (i) (ii)). By Bolzano_Weierstrass_gen it holds that (∃ (n : ℕ → ℕ), is_index_seq n ∧ Un_cv (fun (k : ℕ) ↦ a (n k)) (proj1_sig (_,_,lim_sup_bdd a (i) (iii)))) (iv). Obtain such an n0. It holds that (is_index_seq n0 ∧ Un_cv (fun (k : ℕ) ↦ a (n0 k)) (proj1_sig (_,_,lim_sup_bdd a (i) (iii)))) (v). Choose n := n0. Choose l := (proj1_sig (_,_,lim_sup_bdd a (i) (iii))). By (v) it suffices to show that (is_index_seq n ∧ Un_cv (fun k ↦ a(n(k)), proj1_sig (_,_,lim_sup_bdd a (i) (iii)))). By (v) we conclude that (is_index_seq n ∧ Un_cv (fun k ↦ a(n(k)), proj1_sig (_,_,lim_sup_bdd a (i) (iii)))). 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