lookup_union_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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