English
Let f be a countably generated filter on a set and u: ℕ → α a sequence. If the meet f ⊓ map u atTop is nontrivial, then there exists a strictly increasing θ: ℕ → ℕ such that u ∘ θ tends to f along atTop.
Русский
Пусть f — фильтр на некотором множестве, порожденный счётным образом, и задана последовательность u: ℕ → α. Если пересечение фильтра f и образа через u фильтра atTop не нулевой, то существует строго возрастaющая θ: ℕ → ℕ такая, что u ∘ θ сходится к f по atTop.
LaTeX
$$$\\text{NeBot}(f \\cap \\text{map }u\\,\\text{atTop}) \\Rightarrow \\exists \\theta: \\mathbb{N} \\to \\mathbb{N},\\ \\text{StrictMono}(\\theta) \\land \\ Tendsto (u \\circ \\theta)\\ atTop\\ f.$$$
Lean4
theorem subseq_tendsto_of_neBot {f : Filter α} [IsCountablyGenerated f] {u : ℕ → α} (hx : NeBot (f ⊓ map u atTop)) :
∃ θ : ℕ → ℕ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f :=
by
rw [← Filter.push_pull', map_neBot_iff] at hx
rcases exists_seq_tendsto (comap u f ⊓ atTop) with ⟨φ, hφ⟩
rw [tendsto_inf, tendsto_comap_iff] at hφ
obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ StrictMono (φ ∘ ψ) := strictMono_subseq_of_tendsto_atTop hφ.2
exact ⟨φ ∘ ψ, hψφ, hφ.1.comp hψ.tendsto_atTop⟩
