erase_erase — Mathlib

English

Erasing a then a' equals erasing a' then a: erase a (erase a' s) = erase a' (erase a s).

Русский

Стирание сначала a, затем a' равно стиранию сначала a', затем a: erase a (erase a' s) = erase a' (erase a s).

LaTeX

$$$ erase\ a\ (erase\ a'\ s) = erase\ a'\ (erase\ a\ s) $$$

Lean4

theorem erase_erase {a a' : α} {s : Finmap β} : erase a (erase a' s) = erase a' (erase a s) :=
  induction_on s fun s => ext (by simp only [AList.erase_erase, erase_toFinmap])

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