English
A version of the previous lemma under the assumption that β is a compactly generated space; ensures existence of u ∈ f with closure(image2 ϕ u s) ⊆ open neighborhood.
Русский
Версия леммы под условием компактности пространства β, гарантирующая существование u ∈ f с closure(image2 ϕ u s) ⊆ открытое окрестное.
LaTeX
$$$ \exists u \in f, \overline{image2 ϕ u s} \subseteq n \quad\text{при дополнительных предположениях.}$$$
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' {c : Set β} (hc₁ : IsCompact c)
(hc₂ : ∃ v ∈ f, closure (image2 ϕ v s) ⊆ c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : ω f ϕ s ⊆ n) :
∃ u ∈ f, closure (image2 ϕ u s) ⊆ n := by
rcases hc₂ with ⟨v, hv₁, hv₂⟩
let k := closure (image2 ϕ v s)
have hk : IsCompact (k \ n) := (hc₁.of_isClosed_subset isClosed_closure hv₂).diff hn₁
let j u := (closure (image2 ϕ (u ∩ v) s))ᶜ
have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
have hj₂ : k \ n ⊆ ⋃ u ∈ f, j u :=
by
have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
rw [this, diff_subset_comm, diff_iUnion]
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
simp_rw [j, diff_compl]
rw [← inter_iInter]
exact Subset.trans inter_subset_right hn₂
rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩
let w := (⋂ u ∈ g, u) ∩ v
have hw₂ : w ∈ f := by simpa [w, *]
have hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ :=
by
apply Subset.trans hg₃
simp only [j, iUnion_subset_iff, compl_subset_compl]
intro u hu
unfold w
gcongr
refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)
all_goals exact Subset.rfl
have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ :=
by
simp only [compl_subset_compl]
exact closure_mono (image2_subset inter_subset_right Subset.rfl)
have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, diff_eq, inter_comm]
have hw : closure (image2 ϕ w s) ⊆ n := compl_subset_compl.mp (Subset.trans hnc (union_subset hw₃ hw₄))
exact ⟨_, hw₂, hw⟩
