mem_support_iff

Mathlib.Data.DFinsupp.Defs

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

English

Equivalent statement to membership in support and nonzero coordinate.

Русский

Эквивалентность между принадлежностью опоре и ненулевой координате.

LaTeX

$$$i \\in f.{\\mathrm{support}} \\iff f_i \\neq 0$$$

Lean4

theorem mem_support_iff {f : Π₀ i, β i} {i : ι} : i ∈ f.support ↔ f i ≠ 0 :=
  f.mem_support_toFun _

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

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

Разделы

Аффилиация

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