English
The ≤ relation on DegLex is characterized by a two-level comparison: first compare degrees, then, if equal, compare the toLex-values of the degrees.
Русский
Отношение ≤ на DegLex задаётся двухуровневым сравнением: сначала сравниваются степени, затем, при равенстве, сравниваются значения toLex степеней.
LaTeX
$$$x \le y \iff (\operatorname{deg}(\operatorname{ofDegLex}x) < \operatorname{deg}(\operatorname{ofDegLex}y)) \\ \quad \lor \left( \operatorname{deg}(\operatorname{ofDegLex}x) = \operatorname{deg}(\operatorname{ofDegLex}y) \land \operatorname{toLex}(\operatorname{ofDegLex}x) \le \operatorname{toLex}(\operatorname{ofDegLex}y) \right)$$$
Lean4
theorem le_iff {x y : DegLex (α →₀ ℕ)} :
x ≤ y ↔
(ofDegLex x).degree < (ofDegLex y).degree ∨
(ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) :=
by
simp only [le_iff_eq_or_lt, lt_iff, EmbeddingLike.apply_eq_iff_eq]
by_cases h : x = y
· simp [h]
· by_cases k : (ofDegLex x).degree < (ofDegLex y).degree
· simp [k]
· simp only [h, k, false_or]
