mem_lookup_union — Mathlib

English

Membership of b in the lookup of a in the union is equivalent to b being in the lookup of a in s1 or (a ∉ s1 and b in lookup a s2).

Русский

Членство b в lookup(a, s1 ∪ s2) эквивалентно членству в lookup(a, s1) или (a ∉ s1 и b ∈ lookup(a, s2)).

LaTeX

$$$ b \in lookup(a, s_1 \cup s_2) \iff b \in lookup(a, s_1) \lor a \notin s_1 \land b \in lookup(a, s_2) $$$

Lean4

theorem mem_lookup_union {a} {b : β a} {s₁ s₂ : AList β} :
    b ∈ lookup a (s₁ ∪ s₂) ↔ b ∈ lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ lookup a s₂ :=
  mem_dlookup_kunion

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