support_smul

Mathlib.Data.DFinsupp.Module

URI: https://scilib.ai/kg/mathlib#DFinsupp.support_smul

← MathLib Explorer

English

The support of b • v is contained in the support of v.

Русский

Опора элемента b • v содержится в опоре v.

LaTeX

$$$$ \\mathrm{supp}(b \\cdot v) \\subseteq \\mathrm{supp}(v) $$$$

Lean4

theorem support_smul {γ : Type w} [∀ i, Zero (β i)] [∀ i, SMulZeroClass γ (β i)]
    [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (b : γ) (v : Π₀ i, β i) : (b • v).support ⊆ v.support :=
  support_mapRange

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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