support_single_subset

Mathlib.Data.DFinsupp.Defs

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

English

The support of a singleton is contained in {i}.

Русский

Опора одинарного элемента содержится в {i}.

LaTeX

$$$(\\mathrm{single}_i b).\\operatorname{support} \\subseteq \\{ i \\}$$$

Lean4

theorem support_single_subset {i : ι} {b : β i} : (single i b).support ⊆ { i } :=
  support_mk'_subset

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

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

Разделы

Аффилиация

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