degLex_lt_iff — Mathlib

English

For all a,b in σ →₀ ℕ, a is strictly less than b under degLex if and only if the degLex embedding shows a < b.

Русский

Для любых a,b ∈ σ →₀ ℕ, a ≺_{degLex} b тогда и только тогда, когда их образ в degLex имеет отношение <.

LaTeX

$$$$ a \\prec_{degLex} b \\;\\Longleftrightarrow\\; toDegLex\\,a < toDegLex\\,b. $$$$

Lean4

theorem degLex_lt_iff {a b : σ →₀ ℕ} : a ≺[degLex] b ↔ toDegLex a < toDegLex b :=
  Iff.rfl

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