support_mul_subset_left

Mathlib.Data.Finsupp.Pointwise

URI: https://scilib.ai/kg/mathlib#Finsupp.support_mul_subset_left

English

For g1,g2 : ι →₀ β, the support of g1 * g2 is contained in the support of g1.

Русский

Для g1,g2 : ι →₀ β опора умножения g1 * g2 вложена в опору g1.

LaTeX

$$$ (g_1 * g_2).\\operatorname{support} \\subseteq g_1.\\operatorname{support} $$$

Lean4

theorem support_mul_subset_left {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₁.support := fun x hx => by aesop

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

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

Разделы

Аффилиация

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