def Sequences.IsSubsequence (x y : ℕ → ℝ) : Prop

y is a subsequence of x if there is a strictly increasing index function φ : ℕ → ℕ such that y = x ∘ φ (i.e. y k = x (φ k)).

theorem Sequences.bolzano_weierstrass (x : ℕ → ℝ) (hb : Bornology.IsBounded (Set.range x)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (L : ℝ), Filter.Tendsto (x ∘ φ) Filter.atTop (nhds L)

Bolzano–Weierstrass theorem for real sequences: every bounded real sequence has a convergent subsequence, i.e. a strictly increasing φ : ℕ → ℕ and a limit L : ℝ with x ∘ φ → L.

theorem Sequences.subseq_tendsto (x : ℕ → ℝ) (L : ℝ) (φ : ℕ → ℕ) (hφ : StrictMono φ) (hx : Filter.Tendsto x Filter.atTop (nhds L)) : Filter.Tendsto (x ∘ φ) Filter.atTop (nhds L)

If a real sequence x converges to L, then every subsequence x ∘ φ (with φ : ℕ → ℕ strictly increasing) also converges to L.