proposition: Lemma exists_good_subseq : ∀ (a : ℕ → ℝ) (P : ℕ → ℝ → Prop), (∀ (m : ℕ) (N : ℕ), ∃ k : ℕ, (N ≤ k)%nat ∧ (P m (a k))) ⇒ ∃ n : ℕ → ℕ, is_index_seq n ∧ ∀ k : ℕ, P k (a (n k)).
proof: Proof. Take a : (ℕ → ℝ). Take P : (ℕ → ℝ → Prop). Assume that (for all m N : ℕ, there exists k : ℕ , (N ≤ k)%nat ∧ P m (a k)). By existence_next_el_to_fun it holds that (∃ g : ℕ → ℕ → ℕ, ∀ (m : ℕ) (N : ℕ), (N ≤ g m N)%nat ∧ P m (a (g m N))). Obtain such a g. It holds that (∀ (m : ℕ) (N : ℕ), (N ≤ g m N)%nat ∧ P m (a (g m N))) (i). Choose n := (create_seq g). We show both statements. - We need to show that (is_index_seq n). We need to show that (is_index_seq (create_seq g)). By created_seq_is_index_seq it suffices to show that (for all m N : ℕ, (g m N ≥ N)%nat). Take m, M : nat. By (i) it holds that ((M ≤ g m M)%nat ∧ P m (a (g m M))). We conclude that (g m M >= M)%nat. - We need to show that (for all k : ℕ, P k (a (n k))). We need to show that (for all k : ℕ, P k (a ((create_seq g) k))). Fail By subseq_sat_rel it suffices to show that (for all m N : ℕ, P m (a (g m N))). apply subseq_sat_rel. Take m : ℕ. Take M : ℕ. By (i) it holds that ((M ≤ g m M)%nat ∧ P m (a (g m M))) (ii). Because (ii) both (M ≤ g m M)%nat and (P m (a (g m M))) hold. We conclude that (P m (a (g m M))). Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove