English
Let f be a filter on τ and ϕ: τ → α → β. For any nonempty s ⊆ α and y ∈ β, y belongs to the ω-limit of s with respect to f and ϕ iff for every neighborhood n of y, the forward images ϕ t '' s intersect n frequently as t ranges over f.
Русский
Пусть f — фильтр на τ и ϕ: τ → α → β. Пусть s ⊆ α; тогда y принадлежит ω‑лимиту s по отношению к f и ϕ тогда и только тогда, когда для каждой окрестности n точки y множества { t ∈ τ : (ϕ t '' s) ∩ n ≠ ∅ } встречается часто по уровню f.
LaTeX
$$$ y \in \omega f ϕ s \iff \forall n \in 𝓝 y, \exists^f t \in f, (ϕ t '' s \cap n) \neq \emptyset. $$$
Lean4
/-- An element `y` is in the ω-limit set of `s` w.r.t. `f` if the forward images of `s`
frequently (w.r.t. `f`) intersect arbitrary neighbourhoods of `y`. -/
theorem mem_omegaLimit_iff_frequently₂ (y : β) : y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ t in f, (ϕ t '' s ∩ n).Nonempty := by
simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]
