lookup_erase_ne

Mathlib.Data.List.AList

URI: https://scilib.ai/kg/mathlib#AList.lookup_erase_ne

English

If a ≠ a', then lookup a (erase a' s) = lookup a s.

Русский

Если a ≠ a', то lookup a (erase a' s) = lookup a s.

LaTeX

$$a \neq a' \Rightarrow lookup(a,erase(a',s)) = lookup(a,s)$$

Lean4

@[simp]
theorem lookup_erase_ne {a a'} {s : AList β} (h : a ≠ a') : lookup a (erase a' s) = lookup a s :=
  dlookup_kerase_ne h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru