τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.36686
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
v : Set τ
hv : v ∈ f
⊢ (⋂ (u : Set τ) (_ : u ∈ f), closure (image2 ϕ (u ∩ v) s)) = ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.36686
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)
rw [omegaLimit_eq_biInter_inter _ _ _ hv]
no goals
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.36686
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
v : Set τ
hv : v ∈ f
⊢ (⋂ (u : Set τ) (_ : u ∈ f), closure (image2 ϕ (u ∩ v) s)) = ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)
apply biInter_eq_iInter