lookupFinsupp

Mathlib.Data.Finsupp.AList

URI: https://scilib.ai/kg/mathlib#AList.lookupFinsupp

Lean4

/-- Converts an association list into a finitely supported function via `AList.lookup`, sending
absent keys to zero. -/
noncomputable def lookupFinsupp (l : AList fun _x : α => M) : α →₀ M
    where
  support := by
    haveI := Classical.decEq α; haveI := Classical.decEq M
    exact (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset
  toFun
    a :=
    haveI := Classical.decEq α
    (l.lookup a).getD 0
  mem_support_toFun
    a := by
    classical
    simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
    cases lookup a l <;> simp

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

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

Разделы

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

Аффилиация

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