English
Equality of ArchimedeanClass.mk for x and y is equivalent to equality of their orderTop and leadingCoeff.
Русский
Равенство ArchimedeanClass.mk x и ArchimedeanClass.mk y эквивалентно равенству их orderTop и ведущего коэффициента.
LaTeX
$$$ \\mathrm{ArchimedeanClass.mk } x = \\mathrm{ArchimedeanClass.mk } y \\iff (\\mathrm{orderTop}(x) = \\mathrm{orderTop}(y)) \\land (\\mathrm{ArchimedeanClass.mk }(\\mathrm{leadingCoeff} x) = \\mathrm{ArchimedeanClass.mk }(\\mathrm{leadingCoeff} y)) $$$
Lean4
theorem archimedeanClassMk_eq_archimedeanClassMk_iff {x y : Lex (HahnSeries Γ R)} :
ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔
(ofLex x).orderTop = (ofLex y).orderTop ∧
ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff :=
by
rw [le_antisymm_iff, archimedeanClassMk_le_archimedeanClassMk_iff, archimedeanClassMk_le_archimedeanClassMk_iff]
constructor
· simpa +contextual [or_imp, ne_of_gt, le_of_lt] using fun _ ↦ le_antisymm
· intro ⟨horder, hcoeff⟩
exact ⟨.inr ⟨horder, hcoeff.le⟩, .inr ⟨horder.symm, hcoeff.ge⟩⟩
