English
If x: ℕ → ι tends to a limit along atTop and p(x(n)) holds frequently along atTop, then there exists a subsequence (ns) with Tendsto x(ns(n)) atTop and p(x(ns(n))) for all n.
Русский
Если x: ℕ → ι сходится по atTop и p(x(n)) выполняется часто, существует подпоследовательность ns(n), такая что x(ns(n)) сходится по atTop и p выполняется на каждом элементе подпоследовательности.
LaTeX
$$$$\exists \!\text{ns}: \mathbb{N} \to \mathbb{N},\ \operatorname{Tendsto}(\lambda n. x(\text{ns}(n)))\;\operatorname{atTop}\; l \;\land\; \forall n,\ p(x(\text{ns}(n)))$$$$
Lean4
theorem subseq_forall_of_frequently {ι : Type*} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι}
(h_tendsto : Tendsto x atTop l) (h : ∃ᶠ n in atTop, p (x n)) :
∃ ns : ℕ → ℕ, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ n, p (x (ns n)) :=
by
choose ns hge hns using frequently_atTop.1 h
exact ⟨ns, h_tendsto.comp (tendsto_atTop_mono hge tendsto_id), hns⟩
