union_erase — Mathlib

English

Erasing a from the union is the union of erases: erase a (s1 ∪ s2) = erase a s1 ∪ erase a s2.

Русский

Удаление ключа a из объединения равно объединению удалений: erase a (s1 ∪ s2) = erase a s1 ∪ erase a s2.

LaTeX

$$$ \ erase a (s_1 \cup s_2) = \ erase a s_1 \cup \ erase a s_2 $$$

Lean4

theorem union_erase (a : α) (s₁ s₂ : AList β) : erase a (s₁ ∪ s₂) = erase a s₁ ∪ erase a s₂ :=
  ext kunion_kerase.symm

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