lookup_insert — Mathlib

English

For a list s of Sigma β, looking up a in s.toAList equals the deduplicated lookup in s, i.e., lookup a (s.toAList) = s.dlookup a.

Русский

Для списка s из Sigma β поиск a в s.toAList равен поиска в s с удалением дубликатов: lookup a (s.toAList) = s.dlookup a.

LaTeX

$$$ \mathrm{lookup}(a, s^{toAList}) = s^{dlookup}(a) $$$

Lean4

@[simp]
theorem lookup_insert {a} {b : β a} (s : AList β) : lookup a (insert a b s) = some b := by
  simp only [lookup, insert, dlookup_kinsert]

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