degrees_add_of_disjoint — Mathlib

English

If p.degrees and q.degrees are disjoint, then the degree multiset of p + q is the union p.degrees ∪ q.degrees.

Русский

Если p.degrees и q.degrees дизъюнктны, то degrees(p+q) = degrees(p) ∪ degrees(q).

LaTeX

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

Lean4

theorem degrees_add_of_disjoint [DecidableEq σ] (h : Disjoint p.degrees q.degrees) :
    (p + q).degrees = p.degrees ∪ q.degrees :=
  degrees_add_le.antisymm <| Multiset.union_le (le_degrees_add_left h) (le_degrees_add_right h)

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