degLex_le_iff — Mathlib

English

For all a,b in σ →₀ ℕ, a is below b in degLex exactly when their degLex embeddings satisfy the usual ≤ relation.

Русский

Для любых a,b ∈ σ →₀ ℕ неравенство degLex соответствует обычному порядку стратификации по их образу under toDegLex.

LaTeX

$$$$ a \\preceq_{degLex} b \\;\\Longleftrightarrow\\; toDegLex\\,a \\le toDegLex\\,b. $$$$

Lean4

theorem degLex_le_iff {a b : σ →₀ ℕ} : a ≼[degLex] b ↔ toDegLex a ≤ toDegLex b :=
  Iff.rfl

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