English
DegLex r s on α →₀ ℕ is defined by comparing the pair (degree, function) after mapping into a lexicographic product: f < g iff (deg(f), f) < (deg(g), g) under Prod.Lex with degree-order s and coefficient-order Finsupp.Lex r s.
Русский
DegLex r s на α →₀ ℕ задаётся сравнивающим отображением f ↦ (deg f, f) в лексикографическом произведении: f < g тогда и только тогда, когда (deg f, f) < (deg g, g) по порядку Prod.Lex, где первый компонент упорядочивает степени по s, а второй — коэффициенты по Finsupp.Lex r s.
LaTeX
$$$Finsupp.DegLex\, r\, s\ a\ b \;\Longleftrightarrow\; \operatorname{Prod.Lex} \, s \, (\operatorname{Finsupp.Lex} \, r \, s)\, (a.degree, a)\, (b.degree, b)$$$
Lean4
/-- `Finsupp.DegLex r s` is the homogeneous lexicographic order on `α →₀ M`,
where `α` is ordered by `r` and `M` is ordered by `s`.
The type synonym `DegLex (α →₀ M)` has an order given by `Finsupp.DegLex (· < ·) (· < ·)`. -/
protected def DegLex (r : α → α → Prop) (s : ℕ → ℕ → Prop) : (α →₀ ℕ) → (α →₀ ℕ) → Prop :=
(Prod.Lex s (Finsupp.Lex r s)) on (fun x ↦ (x.degree, x))
