proposition: Lemma subsequence_of_convergent_sequence : ∀ a : (ℕ → X), ∀ p : X, a ⟶ p ⇒ ∀ (n : ℕ → ℕ), is_index_sequence n ⇒ (a ◦ n) ⟶ p.
proof: Proof. Take a : (ℕ → X). Take p : X. Assume that (a ⟶ p). Take n : (ℕ → ℕ). Assume that (is_index_sequence n). It suffices to show that (∀ ε : ℝ, ε > 0 ⇒ ∃ N3 : ℕ, ∀ k : ℕ, (k ≥ N3)%nat ⇒ dist _ (a (n k)) p < ε). Take ε : ℝ; such that (ε > 0). It holds that (∃ N3 : ℕ, ∀ k : ℕ, (k ≥ N3)%nat → dist _ (a k) p < ε). Obtain such a K. Choose N3 := K. Take k : ℕ; such that (k ≥ N3)%nat. By index_sequence_property2 it holds that (n k ≥ n K)%nat. By index_sequence_property it holds that (n K ≥ K)%nat. assert (H3 : (n k ≥ K)%nat) by auto with zarith. We conclude that (dist _ (a (n k)) p < ε). Qed.
imports: Coq.Reals.Reals Automation Libs.Analysis.MetricSpaces Libs.Analysis.SequencesMetric Notations Tactics