English
If α and β are complete lattices, then their Cartesian product α × β, equipped with the product order (a,b) ≤ (a',b') iff a ≤ a' and b ≤ b', is also a complete lattice. The join and meet are taken componentwise.
Русский
Если α и β — полные решетки, то их декартово произведение α × β с попарным порядком является также полной решеткой; пределы и зводы берутся по координатам.
LaTeX
$$$ \alpha \text{ и } \beta \text{ — полные решетки} \implies (\alpha \times \beta, \le) \text{ — полная решетка, где } (a,b) \le (a',b') \iff a \le a', b \le b' $.$$
Lean4
instance instCompleteLattice [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α × β)
where
__ := instBoundedOrder α β
le_sSup _ _ hab := ⟨le_sSup <| mem_image_of_mem _ hab, le_sSup <| mem_image_of_mem _ hab⟩
sSup_le _ _
h := ⟨sSup_le <| forall_mem_image.2 fun p hp => (h p hp).1, sSup_le <| forall_mem_image.2 fun p hp => (h p hp).2⟩
sInf_le _ _ hab := ⟨sInf_le <| mem_image_of_mem _ hab, sInf_le <| mem_image_of_mem _ hab⟩
le_sInf _ _
h := ⟨le_sInf <| forall_mem_image.2 fun p hp => (h p hp).1, le_sInf <| forall_mem_image.2 fun p hp => (h p hp).2⟩
