insert_insert — Mathlib

English

In an AList, inserting a with value b into s and then inserting a with value b' yields the same result as just inserting a with b'.

Русский

В AList вставка пары с ключом a и значением b в s затем вставка с тем же ключом a и значением b' даёт тот же результат, что и просто вставка a с значением b'.

LaTeX

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

Lean4

@[simp]
theorem insert_insert {a} {b b' : β a} (s : AList β) : (s.insert a b).insert a b' = s.insert a b' := by ext : 1;
  simp only [AList.entries_insert, List.kerase_cons_eq]

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