dlookup_kunion_left — Mathlib

English

If a is in the keys of l1, then looking up a in kunion(l1,l2) yields the same as looking up a in l1.

Русский

Если a принадлежит ключам l1, то поиск a в kunion(l1,l2) равен поиску a в l1.

LaTeX

$$$ a \\in l_1.\\keys \\Rightarrow dlookup(a,kunion(l_1,l_2)) = dlookup(a,l_1) $$$

Lean4

@[simp]
theorem dlookup_kunion_left {a} {l₁ l₂ : List (Sigma β)} (h : a ∈ l₁.keys) : dlookup a (kunion l₁ l₂) = dlookup a l₁ :=
  by
  induction l₁ generalizing l₂ with
  | nil => simp at h
  | cons s _ ih =>
    simp only [keys_cons, mem_cons] at h
    rcases h with rfl | h <;> obtain ⟨a'⟩ := s
    · simp
    · rw [kunion_cons]
      by_cases h' : a = a'
      · subst h'
        simp
      · simp [h', ih h]

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