English
Given any filter F on α and sets V(n) ∈ F, for any sequence u: ℕ → α tending to F, there exists a strictly increasing φ: ℕ → ℕ such that u(φ(n)) ∈ V(n) for all n.
Русский
Пусть на α задан фильтр F и множества V(n) ∈ F; для любой последовательности u: ℕ → α, сходящейся к F, существует строго монотонная отображение φ: ℕ → ℕ such that u(φ(n)) ∈ V(n) для всех n.
LaTeX
$$$\forall F:\mathrm{Filter}\ α,\ V:\mathbb{N} \to\mathcal{P}(α),\ (\forall n, V(n)\in F) \to \forall u:\mathbb{N}\to α,\ (Tendsto\ u\ atTop\ F)\to\ \exists \varphi:\mathbb{N}\to\mathbb{N},\ (StrictMono\ \varphi)\wedge\ \forall n:\mathbb{N},\ u(\varphi(n))\in V(n)$$$
Lean4
theorem subseq_mem {F : Filter α} {V : ℕ → Set α} (h : ∀ n, V n ∈ F) {u : ℕ → α} (hu : Tendsto u atTop F) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, u (φ n) ∈ V n :=
extraction_forall_of_eventually' (fun n => tendsto_atTop'.mp hu _ (h n) : ∀ n, ∃ N, ∀ k ≥ N, u k ∈ V n)
