insert_insert_of_ne — Mathlib

English

Inserting at two possibly different keys commutes: (s.insert a b).insert a' b' = (s.insert a' b').insert a b.

Русский

Вставка по двум ключам, возможно разным, коммутирует: (s.insert a b).insert a' b' = (s.insert a' b').insert a b.

LaTeX

$$$ (s.insert a b).insert a' b' = (s.insert a' b').insert a b $$$

Lean4

theorem insert_insert_of_ne {a a'} {b : β a} {b' : β a'} (s : Finmap β) (h : a ≠ a') :
    (s.insert a b).insert a' b' = (s.insert a' b').insert a b :=
  induction_on s fun s => by simp only [insert_toFinmap, AList.toFinmap_eq, AList.insert_insert_of_ne _ h]

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