map_dlookup_eq_find — Mathlib

English

For NodupKeys lists, b ∈ dlookup a l is equivalent to ⟨a,b⟩ ∈ l.

Русский

Для списков с NodupKeys равносильно: b ∈ dlookup a l ⇔ ⟨a,b⟩ ∈ l.

LaTeX

$$$ \\mathrm{NodupKeys}(l) \\Rightarrow (b \\in \\mathrm{dlookup}\,a\,l) \\iff \\langle a,b\\rangle \\in l $$$

Lean4

theorem map_dlookup_eq_find (a : α) (l : List (Sigma β)) :
    (dlookup a l).map (Sigma.mk a) = find? (fun s => a = s.1) l := by
  induction l with
  | nil => grind
  | cons s _ _ => by_cases s.fst = a <;> grind

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