English
If α and β are partially ordered types with top elements ⊤α and ⊤β, then the lexicographic order on the product α × β has a top element, namely the image of (⊤α, ⊤β) under the lexicographic embedding, and this top is ≥ every element of α × β.
Русский
Пусть α и β — множества с частично упорядочением и верхними пределами ∈; Лексикографический порядок на α × β имеет верхний элемент, равный образу (⊤α, ⊤β) под лексикографированием, и этот элемент не меньший любого другого элемента пары.
LaTeX
$$$\\forall a\\in \\alpha\\,\\forall b\\in \\beta:\\; (a,b) \\le_{\\mathrm{lex}} (\\top_\\alpha,\\top_\\beta).$$$
Lean4
instance orderTop [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] : OrderTop (α ×ₗ β)
where
top := toLex ⊤
le_top _ := toLex_mono le_top
