proposition: Lemma equivalent_subsequence_convergence : ∀ (x y : ℕ → X), is_subsequence y x ⇒ ∀ p : X, x ⟶ p ⇒ y ⟶ p.
proof: Proof. Take x, y : (ℕ → X). Assume that (is_subsequence y x). Take p : X. Assume that (x ⟶ p). We need to show that (y ⟶ p). It holds that (∃ m : ℕ → ℕ, is_index_sequence m ∧ ∀ k : ℕ, y k = (x ◦ m) k). Obtain such an m. It holds that (is_index_sequence m ∧ ∀ k : ℕ, y k = (x ◦ m) k) (i). Because (i) both (is_index_sequence m) and (for all k : nat, y k = x (m k)) hold. It suffices to show that (∀ ε : ℝ, ε > 0 ⇒ ∃ N3 : ℕ, ∀ k : ℕ, (k ≥ N3)%nat ⇒ dist _ (y k) p < ε). Take ε : ℝ; such that (ε > 0). It holds that (∃ N3 : ℕ, ∀ k : ℕ, (k ≥ N3)%nat → dist _ (x k) p < ε). Obtain such a K. Choose N3 := K. Take k : ℕ; such that (k ≥ N3)%nat. By index_sequence_property2 it holds that (m k ≥ m K)%nat. By index_sequence_property it holds that (m K ≥ K)%nat. It holds that (m k ≥ K)%nat. It holds that (dist _ (x (m k)) p < ε). It holds that (y k = x (m k)) (iv). rewrite (iv). We conclude that ( dist _ (x (m k)) p < ε). Qed.
imports: Coq.Reals.Reals Automation Libs.Analysis.MetricSpaces Libs.Analysis.SequencesMetric Notations Tactics