mem_lookupAll — Mathlib

English

The list obtained by mapping each element of lookupAll a l back to a Sigma term by Sigma.mk a is a sublist of l.

Русский

Список, полученный апокодированием каждого элемента lookupAll a l обратно в Sigma через Sigma.mk a, является подсписком l.

LaTeX

$$$ (\mathrm{lookupAll} a l).\mathrm{map}(\mathrm{Sigma.mk} a) <+ l $$$

Lean4

theorem mem_lookupAll {a : α} {b : β a} : ∀ {l : List (Sigma β)}, b ∈ lookupAll a l ↔ Sigma.mk a b ∈ l
  | [] => by simp
  | ⟨a', b'⟩ :: l => by
    by_cases h : a = a'
    · subst h
      simp [*, mem_lookupAll]
    · simp [*, mem_lookupAll]

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