English
Applying the Lex isomorphism to the finiteArchimedeanClassOrderIsoLex Lex object yields that the first component corresponds to the leading orderTop.
Русский
Применяя лексическое изоморфное отображение к объекту finiteArchimedeanClassOrderIsoLex, получаем, что первая компонента совпадает с orderTop.
LaTeX
$$$ (\\mathrm{ofLex} (\\mathrm{finiteArchimedeanClassOrderIsoLex } \\Gamma R (\\mathrm{FiniteArchimedeanClass.mk} x\, h))).1 = (\\mathrm{ofLex} x).\\mathrm{orderTop} $$$
Lean4
/-- Finite archimedean classes of `Lex (HahnSeries Γ R)` decompose into lexicographical pairs
of `order` and the finite archimedean class of `leadingCoeff`. -/
noncomputable def finiteArchimedeanClassOrderHomLex :
FiniteArchimedeanClass (Lex (HahnSeries Γ R)) →o Γ ×ₗ FiniteArchimedeanClass R :=
FiniteArchimedeanClass.liftOrderHom
(fun ⟨x, hx⟩ ↦
toLex
⟨(ofLex x).orderTop.untop (by simp [orderTop_of_ne_zero (show ofLex x ≠ 0 by exact hx)]),
FiniteArchimedeanClass.mk (ofLex x).leadingCoeff (leadingCoeff_ne_zero.mpr hx)⟩)
fun ⟨a, ha⟩ ⟨b, hb⟩ h ↦ by
rw [Prod.Lex.le_iff]
simp only [ofLex_toLex]
rw [FiniteArchimedeanClass.mk_le_mk] at ⊢ h
rw [WithTop.untop_eq_iff]
simpa using archimedeanClassMk_le_archimedeanClassMk_iff.mp h
