α : Type u_1
β : Type u_2
γ : Type ?u.3562
δ : Type ?u.3565
ι : Sort ?u.3568
s✝ : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
⊢ {a | ∀ (b : β), b ∈ univ → (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
α : Type u_1
β : Type u_2
γ : Type ?u.3562
δ : Type ?u.3565
ι : Sort ?u.3568
s✝ : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
rw [← principal_univ, mem_prod_principal]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3562
δ : Type ?u.3565
ι : Sort ?u.3568
s✝ : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
⊢ {a | ∀ (b : β), b ∈ univ → (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
simp only [mem_univ, forall_true_left]