English
Let α and β be types equipped with a (<) relation. On the product α × β, there is the standard lexicographic order: compare the first components first; if they are equal, compare the second components. Then for x = (a,b) and y = (a',b') we have x < y in the lexicographic order iff a < a' or (a = a' and b < b').
Русский
Пусть α и β — множества с порядком. На произведении α × β существует лексикографический порядок: сначала сравниваем первые координаты, если они равны, — вторые координаты. Тогда для x=(a,b) и y=(a',b') верно: x < y в лексикографическом порядке тогда и только тогда, когда a < a' или (a = a' и b < b').
LaTeX
$$$$ (a,b) <_{\mathrm{lex}} (a',b') \iff a < a' \lor (a = a' \land b < b'). $$$$
Lean4
theorem toLex_lt_toLex [LT α] [LT β] {x y : α × β} : toLex x < toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 :=
Prod.lex_def
