keys_insert — Mathlib

English

The keys of the inserted AList insert a b s are exactly a followed by the keys of s with a erased.

Русский

Ключи вставки a b s равны списку, начинающемуся ключом a, за которым следует список ключей s без ключа a.

LaTeX

$$$ (\mathrm{insert}(a, b, s)).\mathrm{keys} = a \\;::\\; (s.\mathrm{keys}).\mathrm{erase} \\ a $$$

Lean4

@[simp]
theorem keys_insert {a} {b : β a} (s : AList β) : (insert a b s).keys = a :: s.keys.erase a := by
  simp [insert, keys, keys_kerase]

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