insert_lookupFinsupp — Mathlib

English

Inserting a new value m at index a in l shifts through to look up Finsupp as an update at a.

Русский

Добавление значения $m$ по индексу $a$ в $l$ приводит к тому, что lookupFinsupp новой функции равен обновлённой lookupFinsupp на $a$.

LaTeX

$$$ (l.insert a m).lookupFinsupp = l.lookupFinsupp.update a m$$$

Lean4

@[simp]
theorem insert_lookupFinsupp [DecidableEq α] (l : AList fun _x : α => M) (a : α) (m : M) :
    (l.insert a m).lookupFinsupp = l.lookupFinsupp.update a m :=
  by
  ext b
  by_cases h : b = a <;> simp [h]

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