mem_toAlist

Mathlib.Data.Finsupp.AList

URI: https://scilib.ai/kg/mathlib#Finsupp.mem_toAlist

← MathLib Explorer

English

An index x belongs to the AList encoding of f iff f(x) ≠ 0.

Русский

Указатель x входит в кодировку AList функции f тогда и только тогда, когда f(x) ≠ 0.

LaTeX

$$$x \\in \\mathrm{AList}(f) \\iff f(x) \\neq 0$$$

Lean4

@[simp]
theorem mem_toAlist {f : α →₀ M} {x : α} : x ∈ f.toAList ↔ f x ≠ 0 := by
  classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]

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

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

Разделы

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

Аффилиация

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