English
If α and β are partially ordered with bounds (i.e., bounded orders), then the lexicographic product Lex(α × β) is a bounded order; its bottom and top are the lexicographic images of the respective bounds.
Русский
Если α и β — частично упорядоченные множества с нижними и верхними пределами, то лексикографическое произведение Lex(α × β) является ограниченным порядком; нижняя и верхняя границы получаются как лексикографические образы соответствующих границ пар.
LaTeX
$$$\\text{bot}_{\\mathrm{Lex}} = \\mathrm{toLex}(\\perp_α,\\perp_β) \\quad\\text{and}\\quad \\text{top}_{\\mathrm{Lex}} = \\mathrm{toLex}(\\top_α,\\top_β).$$$
Lean4
instance boundedOrder [PartialOrder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] : BoundedOrder (α ×ₗ β) :=
{ Lex.orderBot, Lex.orderTop with }
