order_abs — Mathlib

English

Absence of order is preserved when taking the absolute value of Lex(HahnSeries Γ R).

Русский

Сохранение порядка при взятии модуля для Lex(HahnSeries Γ R).

LaTeX

$$$ (\\mathrm{ofLex} (|x|)).\\mathrm{orderTop} = (\\mathrm{ofLex} x).\\mathrm{orderTop} $$$

Lean4

theorem order_abs [Zero Γ] (x : Lex (HahnSeries Γ R)) : (ofLex |x|).order = (ofLex x).order :=
  by
  obtain rfl | hne := eq_or_ne x 0
  · simp
  · have hne' : ofLex x ≠ 0 := hne
    have habs : ofLex |x| ≠ 0 := by simpa using hne
    apply WithTop.coe_injective
    rw [order_eq_orderTop_of_ne_zero habs, order_eq_orderTop_of_ne_zero hne']
    apply orderTop_abs

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