degLex_def — Mathlib

English

The DegLex order on α →₀ ℕ agrees with the Prod.Lex comparison of the paired data (degree, function).

Русский

Порядок DegLex на α →₀ ℕ совпадает с сравнением Prod.Lex для пары (степень, функция).

LaTeX

$$$Finsupp.DegLex\, r\, s\ a\ b \iff \mathrm{Prod.Lex}\, s \, (\mathrm{Finsupp.Lex}\, r\ s)\, (a.degree, a)\, (b.degree, b)$$$

Lean4

theorem degLex_def {r : α → α → Prop} {s : ℕ → ℕ → Prop} {a b : α →₀ ℕ} :
    Finsupp.DegLex r s a b ↔ Prod.Lex s (Finsupp.Lex r s) (a.degree, a) (b.degree, b) :=
  Iff.rfl

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