lookup_union_right — Mathlib

English

If a ∉ s1, then lookup a (s1 ∪ s2) = lookup a s2.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lookup_union_right {a} {s₁ s₂ : Finmap β} : a ∉ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₂ :=
  induction_on₂ s₁ s₂ fun _ _ => AList.lookup_union_right

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