lookup_to_alist — Mathlib

English

For any a, the lookup in the alist constructed from a List of Sigma β coincides with the corresponding dlookup on the list.

Русский

Для любого a поиск в AList, полученном из списка List (Sigma β), совпадает с соответствующим dlookup на этом списке.

LaTeX

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

Lean4

@[simp]
theorem lookup_to_alist {a} (s : List (Sigma β)) : lookup a s.toAList = s.dlookup a := by
  rw [List.toAList, lookup, dlookup_dedupKeys]

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