degLex_single_le_iff — Mathlib

English

When comparing singleton monomials of degree 1, single a 1 ≤ single b 1 in degLex is equivalent to b ≤ a in σ.

Русский

При сравнении одинарных мономов степени 1, равенство degLex между single a 1 и single b 1 эквивалентно тому, что b ≤ a в σ.

LaTeX

$$$$ \\text{single } a\\, 1 \\preceq_{degLex} \\text{single } b\\, 1 \\;\\Longleftrightarrow\\; b \\le a. $$$$

Lean4

theorem degLex_single_le_iff {a b : σ} : single a 1 ≼[degLex] single b 1 ↔ b ≤ a := by
  rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]

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