simpa only [← coe_inj] using Set.prod_eq_empty_iff
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L M✝ : Sublattice α
f : LatticeHom α β
s t : Set α
a : α
M : Sublattice β
⊢ L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥
no goals