leadingCoeff_nonneg_iff — Mathlib

English

The nonnegativity of the leading coefficient of the Lex image corresponds to the nonnegativity of the original Hahn series.

Русский

Ненегативность ведущего коэффициента изображения в Lex соответствует неотрицательности исходного ряда Хана.

LaTeX

$$$ 0 \\le (\\mathrm{ofLex } x).\\mathrm{leadingCoeff} \\iff 0 \\le x $$$

Lean4

theorem leadingCoeff_nonneg_iff {x : Lex (HahnSeries Γ R)} : 0 ≤ (ofLex x).leadingCoeff ↔ 0 ≤ x :=
  by
  constructor
  · intro h
    obtain heq | hlt := h.eq_or_lt
    · exact le_of_eq (leadingCoeff_eq_zero.mp heq.symm).symm
    · exact (leadingCoeff_pos_iff.mp hlt).le
  · intro h
    obtain rfl | hlt := h.eq_or_lt
    · simp
    · exact (leadingCoeff_pos_iff.mpr hlt).le

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