mem_lookup_union_middle — Mathlib

English

If b is in the lookup of a in s1 ∪ s3 and a ∉ s2, then b is in the lookup of a in s1 ∪ s2 ∪ s3.

Русский

Если b содержится в lookup(a, s1 ∪ s3) и a не в s2, то b содержится в lookup(a, s1 ∪ s2 ∪ s3).

LaTeX

$$$ b \in lookup(a, s_1 \cup s_3) \rightarrow a \notin s_2 \rightarrow b \in lookup(a, s_1 \cup s_2 \cup s_3) $$$

Lean4

theorem mem_lookup_union_middle {a} {b : β a} {s₁ s₂ s₃ : AList β} :
    b ∈ lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ lookup a (s₁ ∪ s₂ ∪ s₃) :=
  mem_dlookup_kunion_middle

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