dlookup_kinsert_ne — Mathlib

English

If a ≠ a', then dlookup a (kinsert a' b' l) = dlookup a l; inserting a' does not affect the value at a.

Русский

Если a ≠ a', то dlookup a (kinsert a' b' l) = dlookup a l; вставка a' не изменяет значение по ключу a.

LaTeX

$$$a \\neq a' \\Rightarrow dlookup\\ a (kinsert a' b' l) = dlookup\\ a l$$$

Lean4

theorem dlookup_kinsert_ne {a a'} {b' : β a'} {l : List (Sigma β)} (h : a ≠ a') :
    dlookup a (kinsert a' b' l) = dlookup a l := by simp [h]

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