instLinearOrderLex — Mathlib

English

There is a total (linear) order on Lex(HahnSeries Γ R) extending the coefficient-wise order, i.e., Lex(HahnSeries Γ R) is a linear ordered set under the lexicographic comparison of coefficients.

Русский

Существует линейный порядок на Lex(HahnSeries Γ R), расширяющий порядок по коэффициентам, то есть Lex(HahnSeries Γ R) образует линейно упорядованный множество по лексикографическому сопоставлению коэффициентов.

LaTeX

$$$ \\text{LinearOrder } (\\mathrm{Lex} (\\mathrm{HahnSeries} \\ Γ \\ R)) $$$

Lean4

noncomputable instance : LinearOrder (Lex (HahnSeries Γ R))
    where
  le_total a
    b := by
    rcases eq_or_ne a b with hab | hab
    · exact Or.inl hab.le
    · have hab := Function.ne_iff.mp <| HahnSeries.ext_iff.ne.mp hab
      let u := {i : Γ | (ofLex a).coeff i ≠ 0} ∪ {i : Γ | (ofLex b).coeff i ≠ 0}
      let v := {i : Γ | (ofLex a).coeff i ≠ (ofLex b).coeff i}
      have hvu : v ⊆ u := by
        intro i h
        rw [Set.mem_union, Set.mem_setOf_eq, Set.mem_setOf_eq]
        contrapose! h
        rw [Set.notMem_setOf_iff, not_not, h.1, h.2]
      have hv : v.IsWF := ((ofLex a).isPWO_support'.isWF.union (ofLex b).isPWO_support'.isWF).subset hvu
      let i := hv.min hab
      have hji (j) : j < i → (ofLex a).coeff j = (ofLex b).coeff j := not_imp_not.mp <| fun h' ↦ hv.not_lt_min hab h'
      have hne : (ofLex a).coeff i ≠ (ofLex b).coeff i := hv.min_mem hab
      obtain hi | hi := lt_or_gt_of_ne hne
      · exact Or.inl (le_of_lt ⟨i, hji, hi⟩)
      · exact Or.inr (le_of_lt ⟨i, fun j hj ↦ (hji j hj).symm, hi⟩)
  toDecidableLE := Classical.decRel _

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