lookup_union_right — Mathlib

English

If a is not in s1, then lookup in the union equals the lookup in s2.

Русский

Если a не принадлежит s1, то поиск в объединении равен поиску во втором множителе.

LaTeX

$$$ a \notin s_1 \Rightarrow \mathrm{lookup}(a, s_1 \cup s_2) = \mathrm{lookup}(a, s_2) $$$

Lean4

@[simp]
theorem lookup_union_right {a} {s₁ s₂ : AList β} : a ∉ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₂ :=
  dlookup_kunion_right

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