lookup_union_left_of_not_in — Mathlib

English

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

Русский

Если a ∉ s2, то lookup a (s1 ∪ s2) = lookup a s1.

LaTeX

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

Lean4

theorem lookup_union_left_of_not_in {a} {s₁ s₂ : Finmap β} (h : a ∉ s₂) : lookup a (s₁ ∪ s₂) = lookup a s₁ :=
  by
  by_cases h' : a ∈ s₁
  · rw [lookup_union_left h']
  · rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']

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