instLinearOrderDegLexNat — Mathlib

English

There is a LinearOrder instance on DegLex(α →₀ ℕ) defined by lifting the embedding into a Lex-based order.

Русский

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

LaTeX

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

Lean4

/-- The linear order on `Finsupp`s obtained by the homogeneous lexicographic ordering. -/
instance : LinearOrder (DegLex (α →₀ ℕ)) :=
  LinearOrder.lift' (fun (f : DegLex (α →₀ ℕ)) ↦ toLex ((ofDegLex f).degree, toLex (ofDegLex f))) (fun f g ↦ by simp)

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