α : Type u_1
β : Type u_2
γ : Type ?u.188893
ι : Sort ?u.188896
κ : ι → Sort ?u.188901
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : LowerSet α
t t₁ t₂ : LowerSet β
x : α × β
⊢ ↑(s ×ˢ t) = ↑⊥ ↔ ↑s = ↑⊥ ∨ ↑t = ↑⊥
α : Type u_1
β : Type u_2
γ : Type ?u.188893
ι : Sort ?u.188896
κ : ι → Sort ?u.188901
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : LowerSet α
t t₁ t₂ : LowerSet β
x : α × β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
simp_rw [SetLike.ext'_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.188893
ι : Sort ?u.188896
κ : ι → Sort ?u.188901
inst✝¹ : Preorder α
inst✝ : Preorder β
s s₁ s₂ : LowerSet α
t t₁ t₂ : LowerSet β
x : α × β
⊢ ↑(s ×ˢ t) = ↑⊥ ↔ ↑s = ↑⊥ ∨ ↑t = ↑⊥
exact prod_eq_empty_iff