singleton_lookupFinsupp — Mathlib

English

The lookupFinsupp of a singleton is the corresponding singleton Finsupp.

Русский

Обозначение lookupFinsupp для единичной функции даёт соответствующую одиночную Finsupp.

LaTeX

$$$(\\mathrm{singleton}\\ a\ m).lookupFinsupp = \\mathrm{Finsupp}.single a m$$$

Lean4

@[simp]
theorem singleton_lookupFinsupp (a : α) (m : M) : (singleton a m).lookupFinsupp = Finsupp.single a m := by
  classical simp [← AList.insert_empty]

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