τ : Type u_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
τ : Type u_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
p : ι → Set α
⊢ (⋃ (i : ι), ω f ϕ (p i)) ⊆ ω f ϕ (⋃ (i : ι), p i)
rw [iUnion_subset_iff]
no goals
τ : Type u_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
exact fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)