finiteArchimedeanClassOrderIsoLex_apply_fst

English

For nonzero x, the first component of the image under finiteArchimedeanClassOrderIsoLex equals the orderTop of ofLex x.

Русский

Для ненулевого x первая компонента изображения через finiteArchimedeanClassOrderIsoLex равна orderTop у ofLex x.

LaTeX

$$$ {x : Lex (HahnSeries Γ R)} (h : x \\neq 0) \\;:\\; (\\mathrm{ofLex} (\\mathrm{finiteArchimedeanClassOrderIsoLex } Γ R (\\mathrm{FiniteArchimedeanClass.mk} x h))).1 = (\\mathrm{ofLex} x).\\mathrm{orderTop} $$$

Lean4

@[simp]
theorem finiteArchimedeanClassOrderIsoLex_apply_fst {x : Lex (HahnSeries Γ R)} (h : x ≠ 0) :
    (ofLex (finiteArchimedeanClassOrderIsoLex Γ R (FiniteArchimedeanClass.mk x h))).1 = (ofLex x).orderTop := by
  simp [finiteArchimedeanClassOrderIsoLex, finiteArchimedeanClassOrderHomLex]

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