archimedeanClassOrderIsoWithTop_apply

English

Applying archimedeanClassOrderIsoWithTop to ArchimedeanClass.mk x yields (ofLex x).orderTop.

Русский

Применение archimedeanClassOrderIsoWithTop к ArchimedeanClass.mk x дает (ofLex x).orderTop.

LaTeX

$$$\mathrm{archimedeanClassOrderIsoWithTop}(\Gamma, R)(\mathrm{ArchimedeanClass.mk}(x)) = (\mathrm{ofLex}(x)).\mathrm{orderTop}$$$

Lean4

@[simp]
theorem archimedeanClassOrderIsoWithTop_apply (x : Lex (HahnSeries Γ R)) :
    archimedeanClassOrderIsoWithTop Γ R (ArchimedeanClass.mk x) = (ofLex x).orderTop :=
  by
  unfold archimedeanClassOrderIsoWithTop
  obtain rfl | h := eq_or_ne x 0 <;> simp [FiniteArchimedeanClass.withTopOrderIso_symm_apply, *]

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