mem_lookup_union — Mathlib

English

For Finmap β, b ∈ lookup a (s1 ∪ s2) iff b ∈ lookup a s1 or (a ∉ s1 ∧ b ∈ lookup a s2).

Русский

Для Finmap β выполняется: b ∈ lookup a (s1 ∪ s2) эквивалентно b ∈ 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 \bigl( a \notin s_1 \land b \in lookup\ a s_2 \bigr) $$$

Lean4

theorem mem_lookup_union {a} {b : β a} {s₁ s₂ : Finmap β} :
    b ∈ lookup a (s₁ ∪ s₂) ↔ b ∈ lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ lookup a s₂ :=
  induction_on₂ s₁ s₂ fun _ _ => AList.mem_lookup_union

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