archimedeanClassMk_le_archimedeanClassMk_iff

English

For Lex(HahnSeries Γ R), ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y iff either orderTop comparison or equal orders with leadingCoeff comparison.

Русский

Для Lex(HahnSeries Γ R) неравенство ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y эквивалентно либо порядку по orderTop, либо равенству orderTop и сравненю ведущего коэффициента.

LaTeX

$$$ \\text{archimedeanClassMk_le_archimedeanClassMk_iff } {x y : Lex (HahnSeries Γ R)} : \\mathrm{ArchimedeanClass.mk } x ≤ \\mathrm{ArchimedeanClass.mk } y \\iff \\text{(orderTop comparison) or (orderTop equal and leadingCoeff comparison)}$$$

Lean4

theorem archimedeanClassMk_le_archimedeanClassMk_iff {x y : Lex (HahnSeries Γ R)} :
    ArchimedeanClass.mk x ≤ .mk y ↔
      (ofLex x).orderTop < (ofLex y).orderTop ∨
        (ofLex x).orderTop = (ofLex y).orderTop ∧
          ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ .mk (ofLex y).leadingCoeff :=
  by
  obtain hlt | heq | hgt := lt_trichotomy (ofLex x).orderTop (ofLex y).orderTop
  · -- when `x`'s order is less than `y`'s, this reduces to abs_lt_abs_of_orderTop_ofLex
    simpa [ArchimedeanClass.mk_le_mk, hlt] using ⟨1, by simpa using (abs_lt_abs_of_orderTop_ofLex hlt).le⟩
  · -- when `x` and `y` have the same order, this reduces to
        -- `archimedeanClass_le_iff_of_orderTop_eq`
    simpa [heq] using archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex heq
  simp_rw [ArchimedeanClass.mk_le_mk]
  refine ⟨?_, by simp [hgt.not_gt, hgt.ne']⟩
  intro ⟨n, hn⟩
  contrapose! hn
  rw [← abs_nsmul]
  have hgt' : (ofLex y).orderTop < (ofLex (n • x)).orderTop :=
    by
    apply lt_of_lt_of_le hgt
    simpa using orderTop_smul_not_lt n (ofLex x)
  exact abs_lt_abs_of_orderTop_ofLex hgt'

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