lex — Mathlib

English

For c,d in Finsupp, c ≼[lex] d iff toLex c ≤ toLex d; i.e., lex comparison corresponds to the toLex embedding.

Русский

Для c,d ∈ Finsupp: c ≼[lex] d эквивалентно toLex c ≤ toLex d.

LaTeX

$$$$ c \\preceq_{lex} d \\iff toLex\\,c \\le toLex\\,d. $$$$

Lean4

/-- The lexicographic order on `σ →₀ ℕ`, as a `MonomialOrder` -/
noncomputable def lex [WellFoundedGT σ] : MonomialOrder σ
    where
  syn := Lex (σ →₀ ℕ)
  toSyn :=
    { toEquiv := toLex
      map_add' := toLex_add }
  toSyn_monotone := Finsupp.toLex_monotone

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