English
There exists a strictly monotone linear map from M into Lex(HahnSeries(FiniteArchimedeanClass M) R) that aligns Archimedean classes with HahnSeries order top, provided a seed exists; the maximal partial embedding yields the result.
Русский
Существует строго монотонное линейное отображение из M в Lex(HahnSeries(...)), согласующее ArchimedeanClass с orderTop; существование поселенного зерна (seed) обеспечивает существование, а максимальное частичное вложение достигает цели.
LaTeX
$$$\\exists f : M \\to_\\mathbb{K}^\\mathrm{lex}\\; (HahnSeries(\\mathrm{FiniteArchimedeanClass} M)\\; R),\\; \\text{StrictMono}(f) \\land \\forall a, mk(a)=\\mathrm{withTopIso}(M, ofLex(f(a))).orderTop$$$
Lean4
theorem isPartial_sSupFun [IsOrderedAddMonoid R] {c : Set (Partial seed)} (hnonempty : c.Nonempty)
(hc : DirectedOn (· ≤ ·) c) : IsPartial seed (sSupFun hc)
where
strictMono := sSupFun_strictMono hnonempty hc
baseEmbedding_le := baseEmbedding_le_sSupFun hnonempty hc
truncLT_mem_range := truncLT_mem_range_sSupFun hnonempty hc
