kextract_eq_dlookup_kerase — Mathlib

English

Equivalently, for all a and l, kextract a l equals (dlookup a l, kerase a l).

Русский

Эквивалентно: для всех a и l kextract a l равно (dlookup a l, kerase a l).

LaTeX

$$$kextract\\ a\\ l = (dlookup\\ a\\ l, kerase\\ a\\ l)$$$

Lean4

@[simp]
theorem kextract_eq_dlookup_kerase (a : α) : ∀ l : List (Sigma β), kextract a l = (dlookup a l, kerase a l)
  | [] => rfl
  | ⟨a', b⟩ :: l => by
    simp only [kextract]; split_ifs with h
    · subst a'
      simp [kerase]
    · simp [Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]

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