mem_lookup_union_middle — Mathlib

English

If b ∈ lookup a (s1 ∪ s3) and a ∉ s2, then b ∈ lookup a (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)) \land (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₃ : Finmap β} :
    b ∈ lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ lookup a (s₁ ∪ s₂ ∪ s₃) :=
  induction_on₃ s₁ s₂ s₃ fun _ _ _ => AList.mem_lookup_union_middle

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