insert_singleton_eq — Mathlib

English

Inserting a pair into a singleton with the same key returns a singleton with the new value.

Русский

Вставка пары в синглтон с тем же ключом даёт синглтон с новым значением.

LaTeX

$$$ \mathrm{insert}(a, b, \mathrm{singleton}(a, b')) = \mathrm{singleton}(a, b) $$$

Lean4

@[simp]
theorem insert_singleton_eq {a : α} {b b' : β a} : insert a b (singleton a b') = singleton a b :=
  ext <| by simp only [AList.entries_insert, List.kerase_cons_eq, AList.singleton_entries]

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