support_add

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.support_add

English

The support of a sum is contained in the union of the supports: supp(p+q) ⊆ supp(p) ∪ supp(q).

Русский

Опора суммы подпадает под объединение опор: supp(p+q) ⊆ supp(p) ∪ supp(q).

LaTeX

$$$\operatorname{supp}(p+q) \subseteq \operatorname{supp}(p) \cup \operatorname{supp}(q)$$$

Lean4

theorem support_add : (p + q).support ⊆ p.support ∪ q.support := by simpa [support] using Finsupp.support_add

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru