support_sdiff_support_subset_support_add

English

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

Русский

Разность опор p.support \\ q.support входит в опору p + q.

LaTeX

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

Lean4

theorem support_sdiff_support_subset_support_add [DecidableEq σ] (p q : MvPolynomial σ R) :
    p.support \ q.support ⊆ (p + q).support := by
  intro m hm
  simp only [Classical.not_not, mem_support_iff, Finset.mem_sdiff, Ne] at hm
  simp [hm.2, hm.1]

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