English
For a countably generated filter l, a property p holds eventually along l if and only if for every sequence x: ℕ → ι with x tending to l, p(x_n) holds eventually along the tail of the natural numbers.
Русский
Для фильтра l, который счетообразен, свойство p выполняется «в конечной» по l тогда и только тогда, когда для каждой последовательности x: ℕ → ι, сходящейся к l, свойство p (x_n) выполняется часто в хвосте натуральных чисел.
LaTeX
$$$\\forall l IsCountablyGenerated:\\n(\\forallᶠ n in l, p\\ n) \\iff \\forall x: \\mathbb{N} \\to ι, \\operatorname{Tendsto} x\\ atTop\\ l \\Rightarrow \\forallᶠ n in atTop, p (x n)$$$
Lean4
theorem eventually_iff_seq_eventually {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
(∀ᶠ n in l, p n) ↔ ∀ x : ℕ → ι, Tendsto x atTop l → ∀ᶠ n : ℕ in atTop, p (x n) := by
simpa using tendsto_iff_seq_tendsto (f := id) (l := 𝓟 {x | p x})
