support_single_ne_zero

Mathlib.Data.DFinsupp.Defs

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

← MathLib Explorer

English

If b ≠ 0, then the support of the singleton is exactly {i}.

Русский

Если b ≠ 0, то опора одинарного элемента равна {i}.

LaTeX

$$$\\operatorname{Supp}(\\mathrm{single}_i b) = \\{ i \\}$, если $b \\neq 0$$$

Lean4

theorem support_single_ne_zero {i : ι} {b : β i} (hb : b ≠ 0) : (single i b).support = { i } :=
  by
  ext j; by_cases h : i = j
  · subst h
    simp [hb]
  simp [Ne.symm h, h]

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

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

Разделы

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

Аффилиация

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