English
Let α be ordered by LT and β by LE. For x = (a,b) and y = (a',b') in α × β, x ≤ y in the lexicographic order is equivalent to either the first components satisfy a < a' or they are equal and b ≤ b'.
Русский
Пусть α упорядочено отношением <, β — отношением ≤. Пусть x = (a,b), y = (a',b') в α × β. Тогда x ≤ y в лексикографическом порядке эквивалентно: либо a < a', либо a = a' и b ≤ b'.
LaTeX
$$$$ (a,b) \le_{\mathrm{lex}} (a',b') \iff a < a' \lor (a = a' \land b \le b'). $$$$
Lean4
theorem le_iff [LT α] [LE β] {x y : α ×ₗ β} :
x ≤ y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 ≤ (ofLex y).2 :=
Prod.lex_def
