lookupFinsupp_apply — Mathlib

English

For any a, the a-th coordinate of the Finsupp obtained from l by lookupFinsupp equals the value (l.lookup a) with default 0 if absent.

Русский

Для любого $a$ координата $a$ в функции $l$ через lookupFinsupp равна значению $l.lookup(a)$ с дефолтным нулём, если элемента нет.

LaTeX

$$$\\operatorname{lookupFinsupp}(l,a) = (l.lookup(a)).\\mathrm{getD}(0)$$$

Lean4

@[simp]
theorem lookupFinsupp_apply [DecidableEq α] (l : AList fun _x : α => M) (a : α) :
    l.lookupFinsupp a = (l.lookup a).getD 0 :=
  by
  simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
  congr

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