support_of_subset

Mathlib.Algebra.DirectSum.Basic

URI: https://scilib.ai/kg/mathlib#DirectSum.support_of_subset

English

For any i, b in β_i with not zero, the support of DirectSum.of β i b is exactly {i}.

Русский

Для любого i, b≠0 в β_i опора DirectSum.of β i b равна {i}.

LaTeX

$$$\\mathrm{support}(DirectSum.of\\;β\\;i\\;b) = \\{i\\}$, when $b\\neq 0$.$$

Lean4

theorem support_of_subset [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] {i : ι} {b : β i} : (of _ i b).support ⊆ { i } :=
  DFinsupp.support_single_subset

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

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

Разделы

Аффилиация

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