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