dlookup_kerase — Mathlib

English

If a is in the keys of l, then dlookup a (kerase a l) = none when l has no duplicate keys; otherwise the value is unaffected except for the erased entry. In particular, kerase removes the a-entry from dlookup.

Русский

Если a принадлежит ключам l, то dlookup a (kerase a l) = none при отсутствии повторяющихся ключей; иначе значение остается неизменным за вычетом удаляемого элемента.

LaTeX

$$∀ {a} {l : List (Σ β)} (nd : l.NodupKeys), dlookup a (kerase a l) = none$$

Lean4

@[simp]
theorem dlookup_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) : dlookup a (kerase a l) = none :=
  dlookup_eq_none.mpr (notMem_keys_kerase a nd)

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