English
Equality of orderTop under the withTop iso corresponds to ArchimedeanClass.mk.
Русский
Равенство orderTop при изоморфизме с верхним элементом соответствует ArchimedeanClass.mk.
LaTeX
$$$ (\text{orderTop}) = (\text{ArchimedeanMk}) $$$
Lean4
/-- Archimedean equivalence of input is transferred to `HahnSeries.orderTop` equality. -/
theorem orderTop_eq_iff [IsOrderedAddMonoid R] [Archimedean R] (x y : f.val.domain) :
(ofLex (f.val x)).orderTop = (ofLex (f.val y)).orderTop ↔ mk x.val = mk y.val :=
by
obtain hsubsingleton | hnontrivial := subsingleton_or_nontrivial M
· have : y = x := Subtype.eq <| hsubsingleton.allEq _ _
simp [this]
have hnonempty : Nonempty (FiniteArchimedeanClass M) := inferInstance
obtain c := hnonempty.some
have hnontrivial' : Nontrivial (seed.stratum c) := seed.nontrivial_stratum c.prop
have : Nontrivial R := (seed.strictMono_coeff c).injective.nontrivial
rw [← archimedeanClassMk_eq_iff]
simp_rw [← HahnSeries.archimedeanClassOrderIsoWithTop_apply]
rw [(HahnSeries.archimedeanClassOrderIsoWithTop (FiniteArchimedeanClass M) R).injective.eq_iff]
