English
The omega-limit of a nonempty compact-absorbing configuration is nonempty for a nontrivial filter.
Русский
Ω‑лимит непустой конфигурации существует при не тривиальном фильтре и компактной абсорбции.
LaTeX
$$$ (\omega f ϕ s).Nonempty. $$$
Lean4
/-- The ω-limit of a nonempty set w.r.t. a nontrivial filter is nonempty. -/
theorem nonempty_omegaLimit_of_isCompact_absorbing [NeBot f] {c : Set β} (hc₁ : IsCompact c)
(hc₂ : ∃ v ∈ f, closure (image2 ϕ v s) ⊆ c) (hs : s.Nonempty) : (ω f ϕ s).Nonempty :=
by
rcases hc₂ with ⟨v, hv₁, hv₂⟩
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]
apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
· rintro ⟨u₁, hu₁⟩ ⟨u₂, hu₂⟩
use ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
constructor
all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
· intro u
have hn : (image2 ϕ (u ∩ v) s).Nonempty := Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
exact hn.mono subset_closure
· intro
apply hc₁.of_isClosed_subset isClosed_closure
calc
_ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset inter_subset_right Subset.rfl)
_ ⊆ c := hv₂
· exact fun _ ↦ isClosed_closure
