English
The omega-limit equals an iterated intersection with closures of image2 under finite intersections and refinements by intersections.
Русский
ω‑лимит представляет собой итеративное пересечение замыканий образов через image2 с учётом пересечений.
LaTeX
$$$ \omega f ϕ s = \bigcap_{v \in f} \overline{image2 ϕ (v \cap s) s}. $$$
Lean4
/-- A set is eventually carried into any open neighbourhood of its ω-limit:
if `c` is a compact set such that `closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c` for some `v ∈ f`
and `n` is an open neighbourhood of `ω f ϕ s`, then for some `u ∈ f` we have
`closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n`. -/
theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset [T2Space β] {c : Set β}
(hc₁ : IsCompact c) (hc₂ : ∀ᶠ t in f, MapsTo (ϕ t) s c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : ω f ϕ s ⊆ n) :
∃ u ∈ f, closure (image2 ϕ u s) ⊆ n :=
eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' f ϕ _ hc₁
⟨_, hc₂, closure_minimal (image2_subset_iff.2 fun _t ↦ id) hc₁.isClosed⟩ hn₁ hn₂
