dlookup_kunion_right — Mathlib

English

If a is not in the keys of l1, then dlookup of a on kunion(l1,l2) equals dlookup of a on l2.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem dlookup_kunion_right {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
  | cons _ _ ih => simp_all [not_or]

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