single

Mathlib.Data.Finsupp.Single

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

Lean4

/-- `single a b` is the finitely supported function with value `b` at `a` and zero otherwise. -/
def single (a : α) (b : M) : α →₀ M
    where
  support :=
    haveI := Classical.decEq M
    if b = 0 then ∅ else { a }
  toFun :=
    haveI := Classical.decEq α
    Pi.single a b
  mem_support_toFun
    a' := by
    classical
    obtain rfl | hb := eq_or_ne b 0
    · simp [Pi.single, update]
    rw [if_neg hb, mem_singleton]
    obtain rfl | ha := eq_or_ne a' a
    · simp [hb, Pi.single, update]
    simp [ha]

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

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

Разделы

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

Аффилиация

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