lt_def — Mathlib

English

The less-than relation on DegLex(Finsupp α Nat) is defined by a specific lexicographic comparison of degree and toLex-values.

Русский

Отношение меньше чем на DegLex(Finsupp α Nat) задаётся лексикографическим сравнением пары (degree, toLex …).

LaTeX

$$$ a < b \iff (toLex ((ofDegLex a).degree, toLex (ofDegLex a))) < (toLex ((ofDegLex b).degree, toLex (ofDegLex b))) $$$

Lean4

theorem lt_def [LT α] {a b : DegLex (α →₀ ℕ)} :
    a < b ↔ (toLex ((ofDegLex a).degree, toLex (ofDegLex a))) < (toLex ((ofDegLex b).degree, toLex (ofDegLex b))) :=
  Iff.rfl

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