lt_iff — Mathlib

English

There is a linear order on DegLex(α →₀ ℕ) obtained by lifting the lexicographic order via the embedding f ↦ toLex((ofDegLex f).degree, toLex(ofDegLex f)).

Русский

Существует линейный порядок на DegLex(α →₀ ℕ), получаемый возведением лексикографического порядка через отображение f ↦ toLex((ofDegLex f).degree, toLex(ofDegLex f)).

LaTeX

$$$\text{LinearOrder}\,\DegLex(\alpha \to\_0 \mathbb{N})$$$

Lean4

theorem lt_iff [LT α] {a b : DegLex (α →₀ ℕ)} :
    a < b ↔
      (ofDegLex a).degree < (ofDegLex b).degree ∨
        (((ofDegLex a).degree = (ofDegLex b).degree) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)) :=
  by simp [lt_def, Prod.Lex.toLex_lt_toLex]

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