English
There exists an order isomorphism between the finite Archimedean classes of Lex(HahnSeries Γ, R) and Γ, matching the Archimedean structure of coefficients with the Lex ordering.
Русский
Существует упорядоченный изоморфизм между конечными архимедановыми классами Lex(HahnSeries Γ, R) и Γ, сохраняющий структуру упорядоченности коэффициентов через лексикографический порядок.
LaTeX
$$$\mathrm{finiteArchimedeanClassOrderIso}(\Gamma, R) : \mathrm{FiniteArchimedeanClass}(\mathrm{Lex}(\mathrm HahnSeries Γ R)) \cong_o Γ$$$
Lean4
/-- For `Archimedean` coefficients, there is a correspondence between finite
archimedean classes and `HahnSeries.orderTop` without the top element. -/
noncomputable def finiteArchimedeanClassOrderIso : FiniteArchimedeanClass (Lex (HahnSeries Γ R)) ≃o Γ :=
have : Unique (FiniteArchimedeanClass R) := (nonempty_unique _).some
(finiteArchimedeanClassOrderIsoLex Γ R).trans (Prod.Lex.prodUnique _ _)
