archimedeanClassOrderIsoWithTop — Mathlib

English

There is an order isomorphism between the Archimedean classes of Lex(HahnSeries Γ, R) with top and WithTop Γ, preserving the top structure.

Русский

Между архимедановыми классами Lex(HahnSeries Γ, R) с элементом top и WithTop Γ сохраняется упорядоченный изоморфизм.

LaTeX

$$$\mathrm{archimedeanClassOrderIsoWithTop} : \mathrm{ArchimedeanClass}(\mathrm{Lex}(\mathrm HahnSeries Γ R)) \cong_o \mathrm{WithTop} Γ$$$

Lean4

/-- For `Archimedean` coefficients, there is a correspondence between
archimedean classes (with top) and `HahnSeries.orderTop`. -/
noncomputable def archimedeanClassOrderIsoWithTop : ArchimedeanClass (Lex (HahnSeries Γ R)) ≃o WithTop Γ :=
  (FiniteArchimedeanClass.withTopOrderIso _).symm.trans (finiteArchimedeanClassOrderIso _ _).withTopCongr

Похожие утверждения