le_add_right — Mathlib

English

The degree-lexicographic monomial order is compatible with addition on the right: m(a) ≤ m(a) + m(b) for all a,b.

Русский

Порядок degLex совместим с операцией сложения справа: m(a) ≤ m(a) + m(b) для всех a,b.

LaTeX

$$$$ m.toSyn(a) \\le m.toSyn(a) + m.toSyn(b). $$$$

Lean4

theorem le_add_right (a b : σ →₀ ℕ) : m.toSyn a ≤ m.toSyn a + m.toSyn b :=
  by
  rw [← map_add]
  exact m.toSyn_monotone le_self_add

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