mem_dlookup — Mathlib

English

If l has NodupKeys and ⟨a,b⟩ ∈ l, then b ∈ dlookup a l.

Русский

Если l имеет NodupKeys и ⟨a,b⟩ ∈ l, то b ∈ dlookup a l.

LaTeX

$$$ l.NodupKeys \\land \\langle a,b\\rangle \\in l \\Rightarrow b \\in \\mathrm{dlookup} a\,l $$$

Lean4

theorem mem_dlookup {a} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : Sigma.mk a b ∈ l) : b ∈ dlookup a l :=
  by
  obtain ⟨b', h'⟩ := Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h))
  cases nd.eq_of_mk_mem h (of_mem_dlookup h')
  exact h'

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