erase_erase — Mathlib

English

Erasing a then erasing a' yields the same result as erasing a' then erasing a: (s.erase a).erase a' = (s.erase a').erase a.

Русский

Стирание a затем a' даёт тот же результат, что и стирание a' затем a: (s.erase a).erase a' = (s.erase a').erase a.

LaTeX

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

Lean4

theorem erase_erase (a a' : α) (s : AList β) : (s.erase a).erase a' = (s.erase a').erase a :=
  ext <| kerase_kerase

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