English
An element y is in the ω-limit of s if and only if for every neighborhood n of y, the set of t for which s ∩ ϕ t^{-1}(n) is nonempty is frequently in f.
Русский
Элемент y принадлежит ω-пределу s тогда и только тогда, когда для каждого окрестности n(y) множество t, удовлетворяющее s ∩ ϕ(t)^{-1}(n) непусто, часто встречается в f.
LaTeX
$$$$ y \in \omega f ϕ s \iff \forall n \in 𝓝 y, \exists_f t \in f, (s \cap ϕ t^{-1}(n)).\text{Nonempty}.$$$$
Lean4
/-- An element `y` is in the ω-limit set of `s` w.r.t. `f` if the
preimages of an arbitrary neighbourhood of `y` frequently (w.r.t. `f`) intersects of `s`. -/
theorem mem_omegaLimit_iff_frequently (y : β) : y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ t in f, (s ∩ ϕ t ⁻¹' n).Nonempty :=
by
simp_rw [frequently_iff, omegaLimit_def, mem_iInter, mem_closure_iff_nhds]
constructor
· intro h _ hn _ hu
rcases h _ hu _ hn with ⟨_, _, _, ht, _, hx, rfl⟩
exact ⟨_, ht, _, hx, by rwa [mem_preimage]⟩
· intro h _ hu _ hn
rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
exact ⟨_, hϕtx, _, ht, _, hx, rfl⟩
