mem_dlookup_iff — Mathlib

English

Equivalence form of mem_dlookup under NodupKeys: b ∈ dlookup a l ↔ ⟨a,b⟩ ∈ l.

Русский

Эквивалентность mem_dlookup под NodupKeys: b ∈ dlookup a l ⇔ ⟨a,b⟩ ∈ l.

LaTeX

$$$ \\mathrm{mem\\_dlookup\\_iff} (l,NodupKeys) : (b \\in \\mathrm{dlookup}\\,a\,l) \\iff \\langle a,b\\rangle \\in l $$$

Lean4

theorem mem_dlookup_iff {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) :
    b ∈ dlookup a l ↔ Sigma.mk a b ∈ l :=
  ⟨of_mem_dlookup, mem_dlookup nd⟩

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