dlookup_dedupKeys — Mathlib

English

For any a, the lookup in the deduped list equals the lookup in the original list: dlookup a l.dedupKeys = dlookup a l.

Русский

Для любого a поиск в списке без повторов равен поиску в исходном списке: dlookup a l.dedupKeys = dlookup a l.

LaTeX

$$∀ {a} {l : List (Σ β)}, dlookup a l.dedupKeys = dlookup a l$$

Lean4

theorem dlookup_dedupKeys (a : α) (l : List (Sigma β)) : dlookup a (dedupKeys l) = dlookup a l := by
  induction l with
  | nil => rfl
  | cons l_hd _ l_ih =>
    obtain ⟨a', b⟩ := l_hd
    by_cases h : a = a'
    · subst a'
      rw [dedupKeys_cons, dlookup_kinsert, dlookup_cons_eq]
    · rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]
      exact h

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