proposition: Lemma upp_bd_seq_is_upp_bd_lim : ∀ (a : ℕ → ℝ) (L M: ℝ), (∀ n : ℕ, a n ≤ M) ⇒ (Un_cv a L) ⇒ L ≤ M.
proof: Proof. Take a : (ℕ → ℝ). Take L : ℝ. Take M : ℝ. Assume that (∀ n : ℕ, (a n) ≤ M). Assume that (Un_cv a L) (i). By Rle_or_lt it holds that (L ≤ M ∨ M < L) (ii). Because (ii) either (L ≤ M) or (M < L) holds. - Case (L ≤ M). It follows that (L ≤ M). - Case (M < L). Define ε := (L-M). It holds that (ε > 0). It holds that (for all eps : ℝ, eps > 0 ⇨ there exists N : ℕ, for all n : ℕ, (n ≥ N)%nat ⇨ ｜ a n - L ｜ < eps). It holds that (∃ N : ℕ, ∀n : ℕ, (n ≥ N)%nat ⇒ R_dist (a n) L < ε). Obtain such an Nn. It holds that (|a(Nn) - L| < ε). By Rabs_def2 it holds that (a Nn - L < ε ∧ (- ε < a Nn - L)). It holds that (- ε < a Nn - L). It holds that (a Nn ≤ M). It holds that (- (L - M) < a Nn - L). It follows that (L ≤ M). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations