lt_iff — Mathlib

English

For x = (a,b) and y = (a',b') in α × β with α,β ordered, 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 lt_iff [LT α] [LT β] {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

Похожие утверждения