lookupAll_sublist — Mathlib

English

For any a, (lookupAll a l).map (Sigma.mk a) is a sublist of l.

Русский

Для любого a списоку (lookupAll a l).map (Sigma.mk a) принадлежит l как подсписок.

LaTeX

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

Lean4

theorem lookupAll_sublist (a : α) : ∀ l : List (Sigma β), (lookupAll a l).map (Sigma.mk a) <+ l
  | [] => by simp
  | ⟨a', b'⟩ :: l => by
    by_cases h : a = a'
    · subst h
      simp only [lookupAll_cons_eq, List.map]
      exact (lookupAll_sublist a l).cons₂ _
    · simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
      exact (lookupAll_sublist a l).cons _

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