English
The compare operation on α ×ₗ β equals the lexicographic compare of the first and second coordinates.
Русский
Операция сравнения на α ×ₗ β равна лексикографическому сравнению первая/вторая координат.
LaTeX
$$$$ \text{compare}(\alpha \times_\mathrm{lex} \beta) = \mathrm{compareLex}(\mathrm{compareOn}(\cdot_1), \mathrm{compareOn}(\cdot_2)). $$$$
Lean4
theorem compare_def [Ord α] [Ord β] :
@compare (α ×ₗ β) _ = compareLex (compareOn fun x => (ofLex x).1) (compareOn fun x => (ofLex x).2) :=
rfl