English
For a countably generated filter l, the frequently property of p along l is equivalent to the existence of a sequence x: ℕ → ι tending to l such that p∘x holds frequently along atTop.
Русский
Для фильтра l, который счетно порожден, свойство frequently для p вдоль l эквивалентно существованию последовательности x: ℕ → ι, сходящейся к l, для которой p ∘ x выполняется часто вдоль atTop.
LaTeX
$$$\\operatorname{Frequent}(p, l) \\iff \\exists x:\\mathbb{N} \\to ι, \\operatorname{Tendsto} x\\ atTop\\ l \\land \\operatorname{Frequent}(p \\circ x, atTop)$$$
Lean4
theorem frequently_iff_seq_frequently {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
(∃ᶠ n in l, p n) ↔ ∃ x : ℕ → ι, Tendsto x atTop l ∧ ∃ᶠ n : ℕ in atTop, p (x n) :=
by
simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]
push_neg; rfl
