dlookup_kinsert — Mathlib

English

The value associated with key a in kinsert a b l is b, i.e., lookup yields some b.

Русский

Значение, соответствующее ключу a в kinsert a b l, равно b, то есть поиск возвращает some b.

LaTeX

$$$\\mathrm{dlookup}\\ a\\ (\\mathrm{kinsert}\\ a\\ b\\ l) = \\mathrm{some}\\ b$$$

Lean4

theorem dlookup_kinsert {a} {b : β a} (l : List (Sigma β)) : dlookup a (kinsert a b l) = some b := by
  simp only [kinsert, dlookup_cons_eq]

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