English
Let α be a partially ordered set and β a preorder. The map toLex: α × β → α ×ₗ β is order-preserving from the product order to the lexicographic order. In particular, if (a1, b1) ≤ (a2, b2) in the product order, then toLex(a1, b1) ≤ in the Lex order toLex(a2, b2).
Русский
Пусть α — частично упорядоченное множество, β — предупорядоченное. Отображение toLex: α × β → α ×ₗ β сохраняет порядок: если (a1, b1) ≤ (a2, b2) по произведению, то toLex(a1, b1) ≤ по лексикографическому порядку toLex(a2, b2).
LaTeX
$$$\forall a_1,a_2\in \alpha, \forall b_1,b_2\in \beta,\ ((a_1 \le a_2 \land b_1 \le b_2) \Rightarrow \mathrm{toLex}(a_1,b_1) \le_{\mathrm{Lex}} \mathrm{toLex}(a_2,b_2)).$$$
Lean4
/-- `toLex` as an `OrderHom`. -/
@[simps]
def toLexOrderHom {α β : Type*} [PartialOrder α] [Preorder β] : α × β →o α ×ₗ β
where
toFun := toLex
monotone' := Prod.Lex.toLex_mono
