English
The deg-lexicographic order on the finitely supported functions σ → 0 ℕ defines a MonomialOrder on σ →₀ ℕ.
Русский
degLex-порядок на множествах функций с конечной опорой из σ в ℕ образует порядок мономов.
LaTeX
$$$$ \\degLex \\text{ is a MonomialOrder on } \\sigma \\to_0 \\mathbb{N}. $$$$
Lean4
/-- The deg-lexicographic order on `σ →₀ ℕ`, as a `MonomialOrder` -/
noncomputable def degLex : MonomialOrder σ where
syn := DegLex (σ →₀ ℕ)
toSyn := { toEquiv := toDegLex, map_add' := toDegLex_add }
toSyn_monotone a b
h := by
simp only [AddEquiv.coe_mk, DegLex.le_iff, ofDegLex_toDegLex]
by_cases ha : a.degree < b.degree
· exact Or.inl ha
· refine Or.inr ⟨le_antisymm ?_ (not_lt.mp ha), toLex_monotone h⟩
rw [← add_tsub_cancel_of_le h, degree_add]
exact Nat.le_add_right a.degree (b - a).degree
