English
There is a natural partial order on Lex(HahnSeries Γ R) defined by lifting the pointwise order on the coefficients of the underlying Hahn series; two elements are compared by looking at their first differing coefficient.
Русский
Существует естественный частичный порядок на Lex(HahnSeries Γ R), получаемый при поднятии покомпонентного порядка коэффициентов базового ряда Хана; два элемента сравниваются по первому отличающемуся коэффициенту.
LaTeX
$$$ \\text{PartialOrder } (\\mathrm{Lex} (\\mathrm{HahnSeries} \\ Γ \\ R)) := \\mathrm{PartialOrder}.lift (\\mathrm{toLex} \\lvert \\mathrm{ofLex} \\cdot \\rvert .\\mathrm{coeff}) \\; (\\text{л» это обычный лексикографический порядок коэффициентов})$$$
Lean4
instance : PartialOrder (Lex (HahnSeries Γ R)) :=
PartialOrder.lift (toLex <| ofLex · |>.coeff) fun x y ↦ by simp
