English
There exists a strict monotone rational-linear embedding f from M into Lex(HahnSeries(FiniteArchimedeanClass M) ℝ) with a compatibility condition expressing how Archimedean classes are realized via orderTop and leadingCoeff.
Русский
Существует строгий монотонный линейный надQ вложение f: M → Lex(HahnSeries(FiniteArchimedeanClass M) ℝ), удовлетворяющее указанному условию совместимости ArchimedeanClass и orderTop/leadingCoeff.
LaTeX
$$$ \\exists f : M \\to_{\\mathbb{Q}}^{\\mathrm{LinearMap}} \\; \\mathrm{Lex} (\\mathrm{HahnSeries} (\\mathrm{FiniteArchimedeanClass} M) \\mathbb{R}),\\; \\text{StrictMono } f \\wedge ∀ a,\\; mk a = \\mathrm{FiniteArchimedeanClass.withTopOrderIso M (\\mathrm{ofLex} (f a)).orderTop} $$$
Lean4
theorem hahnEmbedding_isOrderedModule_rat :
∃ f : M →ₗ[ℚ] Lex (HahnSeries (FiniteArchimedeanClass M) ℝ),
StrictMono f ∧ ∀ a, mk a = FiniteArchimedeanClass.withTopOrderIso M (ofLex (f a)).orderTop :=
by apply hahnEmbedding_isOrderedModule
