English
If p i is a family of sets, then the union of their omega-limits is contained in the omega-limit of the union: ⋃ i ω f ϕ (p i) ⊆ ω f ϕ (⋃ i p i).
Русский
Объединение ω‑лимитов по индексу подмножества включено в ω‑лимит объединения: ⋃ i ω f ϕ (p i) ⊆ ω f ϕ (⋃ i p i).
LaTeX
$$$ \bigcup_i \omega f ϕ (p_i) \subseteq \omega f ϕ (\bigcup_i p_i). $$$
Lean4
theorem omegaLimit_union : ω f ϕ (s₁ ∪ s₂) = ω f ϕ s₁ ∪ ω f ϕ s₂ :=
by
ext y; constructor
· simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty,
frequently_or_distrib]
contrapose!
simp only [not_frequently, not_nonempty_iff_eq_empty, ← subset_empty_iff]
rintro ⟨⟨n₁, hn₁, h₁⟩, ⟨n₂, hn₂, h₂⟩⟩
refine ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩
exacts [Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_left,
Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_right]
· rintro (hy | hy)
exacts [omegaLimit_mono_right _ _ subset_union_left hy, omegaLimit_mono_right _ _ subset_union_right hy]
