support_symmDiff_support_subset_support_add

English

The symmetric difference of supports is contained in the support of p + q.

Русский

Симметрическая разность опор содержится в опоре p + q.

LaTeX

$$p.\\text{support} \\Delta q.\\text{support} \\subseteq (p+q).\\text{support}$$

Lean4

theorem support_symmDiff_support_subset_support_add [DecidableEq σ] (p q : MvPolynomial σ R) :
    p.support ∆ q.support ⊆ (p + q).support :=
  by
  rw [symmDiff_def, Finset.sup_eq_union]
  apply Finset.union_subset
  · exact support_sdiff_support_subset_support_add p q
  · rw [add_comm]
    exact support_sdiff_support_subset_support_add q p

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