orderTop_abs — Mathlib

English

The order is preserved by absolute value: the order of the absolute-valued Lex element equals the order of the original Lex element.

Русский

Порядок сохраняется под модулем: порядок элементов Lex после взятия модуля совпадает с исходным порядком.

LaTeX

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

Lean4

@[simp]
theorem orderTop_abs (x : Lex (HahnSeries Γ R)) : (ofLex |x|).orderTop = (ofLex x).orderTop :=
  by
  obtain hle | hge := le_total x 0
  · rw [abs_eq_neg_self.mpr hle, ofLex_neg, orderTop_neg]
  · rw [abs_eq_self.mpr hge]

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