abs_lt_abs_of_orderTop_ofLex — Mathlib

English

If the orderTop of y is strictly less than the orderTop of x, then |x| < |y| in Lex.

Русский

Если orderTop(y) < orderTop(x), то |x| < |y| в Lex.

LaTeX

$$$ (\\text{orderTop} ofLex y).\\mathrm{orderTop} < (\\text{orderTop} ofLex x).\\mathrm{orderTop} \\\\Rightarrow |x| < |y| $$$

Lean4

theorem abs_lt_abs_of_orderTop_ofLex {x y : Lex (HahnSeries Γ R)} (h : (ofLex y).orderTop < (ofLex x).orderTop) :
    |x| < |y| := by
  rw [← orderTop_abs x, ← orderTop_abs y] at h
  refine (lt_iff _ _).mpr ⟨(ofLex |y|).orderTop.untop h.ne_top, ?_, ?_⟩
  · simp +contextual [-orderTop_abs, coeff_eq_zero_of_lt_orderTop, h.trans']
  · simpa [-orderTop_abs, coeff_eq_zero_of_lt_orderTop, coeff_untop_eq_leadingCoeff, h] using h.ne_top

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