degLex_totalDegree_monotone — Mathlib

English

If degLex.degree f is below degLex.degree g in the degLex order, then the total degrees of f and g satisfy totalDegree(f) ≤ totalDegree(g).

Русский

Если degLex.degree f меньше degLex.degree g по порядку degLex, то totalDegree(f) ≤ totalDegree(g).

LaTeX

$$$(\\degLex.degree f) \\preceq_{\\degLex} (\\degLex.degree g) \\Rightarrow f.totalDegree \\le g.totalDegree$$$

Lean4

theorem degLex_totalDegree_monotone (h : degLex.degree f ≼[degLex] degLex.degree g) : f.totalDegree ≤ g.totalDegree :=
  by
  simp only [← MvPolynomial.degree_degLexDegree]
  exact DegLex.monotone_degree h

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