lookupAll_cons_ne

Mathlib.Data.List.Sigma

URI: https://scilib.ai/kg/mathlib#List.lookupAll_cons_ne

English

For any a, the head of the list lookupAll a l equals dlookup a l.

Русский

Для любого a голова списка lookupAll a l равна dlookup a l.

LaTeX

$$$ \mathrm{head?}( \mathrm{lookupAll} a\ l) = \mathrm{dlookup} a\ l $$$

Lean4

@[simp]
theorem lookupAll_cons_ne (l) {a} : ∀ s : Sigma β, a ≠ s.1 → lookupAll a (s :: l) = lookupAll a l
  | ⟨_, _⟩, h => dif_neg h.symm

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

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

Разделы

Аффилиация

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