le_degrees_add_right — Mathlib

English

If the degree multisets of p and q are disjoint, then q.degrees ≤ (p + q).degrees.

Русский

Если множества степеней p и q непересекаются, то q.degrees ⊆ (p + q).degrees.

LaTeX

$$$\operatorname{Disjoint}(p.degrees, q.degrees) \Rightarrow q.degrees \le (p + q).degrees$$$

Lean4

theorem le_degrees_add_right (h : Disjoint p.degrees q.degrees) : q.degrees ≤ (p + q).degrees := by
  simpa [add_comm] using le_degrees_add_left h.symm

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