instIsOrderedAddMonoidLex — Mathlib

English

Lex(HahnSeries Γ R) forms an ordered additive monoid under the natural Lex order.

Русский

Lex(HahnSeries Γ R) образует упорядоченную аддитивную моноиду под естественным лексикографическим порядком.

LaTeX

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

Lean4

instance : IsOrderedAddMonoid (Lex (HahnSeries Γ R)) where
  add_le_add_left a b hab
    c := by
    obtain rfl | hlt := hab.eq_or_lt
    · simp
    · apply le_of_lt
      rw [lt_iff] at hlt ⊢
      obtain ⟨i, hj, hi⟩ := hlt
      refine ⟨i, ?_, ?_⟩
      · intro j hji
        simpa using congrArg ((ofLex c).coeff j + ·) (hj j hji)
      · simpa using add_lt_add_left hi ((ofLex c).coeff i)

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