English
Let a and b be elements of Lex(α →₀ N) with α equipped with a linear order and N with a compatible order. Then a < b if and only if there exists an index i such that for all j < i we have the same coefficient (the ith coefficient is the first place where a and b differ and a(i) < b(i)).
Русский
Пусть a и b принадлежат Lex(α →₀ N) и α упорядочён линейно, N — упорядочено совместимо. Тогда a < b тогда и только тогда, когда существует индекс i, такой что для всех j < i коэффициенты совпадают, и a(i) < b(i).
LaTeX
$$$a < b \\iff \\exists i,\\ (\\forall j,\\ j < i \\Rightarrow \\operatorname{ofLex} a j = \\operatorname{ofLex} b j) \\land \\operatorname{ofLex} a i < \\operatorname{ofLex} b i$$$
Lean4
theorem lex_lt_iff [LT α] [LT N] {a b : Lex (α →₀ N)} :
a < b ↔ ∃ i, (∀ j, j < i → ofLex a j = ofLex b j) ∧ ofLex a i < ofLex b i :=
Finsupp.lex_def
