lookup_union_eq_some — Mathlib

English

The lookup in the union equals some b exactly when either the left lookup is some b or the right lookup is some b with a not in left side.

Русский

Поиск в объединении равен Some b тогда и только тогда, когда левый поиск равен Some b, или правый поиск равен Some b и a не в левой части.

LaTeX

$$$ lookup(a, s_1 \cup s_2) = \mathrm{Some}(b) \iff lookup(a, s_1) = \mathrm{Some}(b) \lor (a \notin s_1 \land lookup(a, s_2) = \mathrm{Some}(b)) $$$

Lean4

@[simp]
theorem lookup_union_eq_some {a} {b : β a} {s₁ s₂ : AList β} :
    lookup a (s₁ ∪ s₂) = some b ↔ lookup a s₁ = some b ∨ a ∉ s₁ ∧ lookup a s₂ = some b :=
  mem_dlookup_kunion

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