Diagonal extraction for predicates on subsequences

Nested extractions have a strictly increasing diagonal. Its tail lies in the range of each fixed stage, so every predicate stable under eventual subsequences holds on the diagonal. The predicates may concern unrelated probability spaces.

theorem BGW.StableTrees.tendsto_comp_of_eventual_subseq {α : Type u_1} {u : ℕ → α} {l : Filter α} {φ ψ : ℕ → ℕ} (hφ : StrictMono φ) (hψ : StrictMono ψ) (hsub : ∃ (N : ℕ), ∀ k ≥ N, ∃ (j : ℕ), ψ k = φ j) (hu : Filter.Tendsto (u ∘ φ) Filter.atTop l) : Filter.Tendsto (u ∘ ψ) Filter.atTop l

A limit along one increasing subsequence is inherited by every increasing sequence whose tail lies in its range.