English
Let l be a countably generated filter on an index set ι and p be a predicate on ι. Then p holds frequently along l if and only if there exists a sequence ns: ℕ → ι such that ns tends to the top along l and p holds for every ns(n).
Русский
Пусть l — фильтр над множством индексов ι, который порожден счётно, и p — предикат на ι. Тогда p встречается чаще по отношению к l тогда и только тогда существует последовательность ns: ℕ → ι такая, что ns сходится к вершине по l и для каждого n выполняется p(ns(n)).
LaTeX
$$$\\bigl(\\exists^\\infty n \\text{ in } l,\\ p(n)\\bigr) \\;\\Longleftrightarrow\\; \\exists ns: \\mathbb{N} \\to \\iota,\\ Tendsto(ns)\\ atTop\\ l \\land \\forall n,\\ p(ns(n)).$$$
Lean4
theorem frequently_iff_seq_forall {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
(∃ᶠ n in l, p n) ↔ ∃ ns : ℕ → ι, Tendsto ns atTop l ∧ ∀ n, p (ns n) :=
⟨exists_seq_forall_of_frequently, fun ⟨_ns, hnsl, hpns⟩ ↦ hnsl.frequently <| Frequently.of_forall hpns⟩
