τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.37203
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
⊢ (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s)) ⊆ closure (image2 ϕ u s)
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.37203
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
⊢ ω f ϕ s ⊆ closure (image2 ϕ u s)
rw [omegaLimit_eq_iInter]
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.37203
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.37203
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
⊢ (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s)) ⊆ closure (image2 ϕ u s)
intro _ hx
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.37203
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.37203
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
rw [mem_iInter] at hx
no goals
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.37203
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
exact hx ⟨u, hu⟩