simp [SetLike.le_def, forall_and]
ι : 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 β
N : Sublattice (α × β)
⊢ N ≤ L.prod M ↔ N ≤ comap (LatticeHom.fst α β) L ∧ N ≤ comap (LatticeHom.snd α β) M
no goals