proposition: Lemma finite_or_find_one : ∀ (a : ℕ → ℝ) (L : ℝ), (∃ N : ℕ, ∀ k : ℕ, (k >= N)%nat ⇒ a k < L) ∨ (∀ m : ℕ, ∃ n : ℕ, (n >= m)%nat ∧ a n ≥ L).
proof: Proof. Take a : (ℕ → ℝ). Take L : ℝ. Define P := (∃ N : ℕ, ∀ k : ℕ, (k >= N)%nat ⇒ a k < L). By classic it holds that (P \/ ~P) (i). Because (i) either P or (¬P) holds. - Case P. left. assumption. - Case (¬P). right. It holds that (~ ∃ N : ℕ, ∀ k : ℕ, (k >= N)%nat ⇒ a k < L) (ii). We conclude that (∀ m : ℕ, ∃ n : ℕ, (n ≥ m)%nat ∧ a n ≥ L). 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