notMem_support_iff

Mathlib.Data.DFinsupp.Defs

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

English

An index i is not in the support exactly when the i-th coordinate equals zero.

Русский

Индекс i не принадлежит опоре тогда и только тогда, когда i-я координата равна нулю.

LaTeX

$$$i \\notin f.{\\mathrm{support}} \\iff f_i = 0$$$

Lean4

theorem notMem_support_iff {f : Π₀ i, β i} {i : ι} : i ∉ f.support ↔ f i = 0 :=
  not_iff_comm.1 mem_support_iff.symm

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

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

Разделы

Аффилиация

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