insert_union — Mathlib

English

Insertion distributes over union on the left: insert a b (s1 ∪ s2) = insert a b s1 ∪ s2.

Русский

Вставка над объединением слева дистрибутивна: insert a b (s1 ∪ s2) = insert a b s1 ∪ s2.

LaTeX

$$$ \operatorname{insert}(a,b, (s_1 \cup s_2)) = \operatorname{insert}(a,b,s_1) \cup s_2 $$$

Lean4

theorem insert_union {a} {b : β a} {s₁ s₂ : Finmap β} : insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂ :=
  induction_on₂ s₁ s₂ fun a₁ a₂ => by simp [AList.insert_union]

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