English
In Lex(HahnSeries Γ R), the order is lexicographic: a < b if and only if there exists i such that all coefficients with index less than i match, and at i the coefficient of a is smaller than that of b.
Русский
В Lex(HahnSeries Γ R) порядок лексикографический: a < b тогда и только тогда, существует индекс i, для которого для всех j<i коэффициенты совпадают, а в i-ом коэффициенте a меньше чем коэффициент b.
LaTeX
$$$ a < b \\iff \\exists i : Γ, (\\forall j : Γ, j < i \\rightarrow (ofLex a).coeff j = (ofLex b).coeff j) \\land (ofLex a).coeff i < (ofLex b).coeff i $$$
Lean4
theorem lt_iff (a b : Lex (HahnSeries Γ R)) :
a < b ↔
∃ (i : Γ), (∀ (j : Γ), j < i → (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i :=
by rfl
