mem_cons_of_mem

Mathlib.Data.Vector.Mem

URI: https://scilib.ai/kg/mathlib#List.Vector.mem_cons_of_mem

English

If a' is in v.toList, then a' is in the cons of a and v.

Русский

Если a' принадлежит v.toList, то a' принадлежит (a ::ᵥ v).toList.

LaTeX

$$$$ a' \in v.toList \Rightarrow a' \in (a ::ᵥ v).toList $$$$

Lean4

theorem mem_cons_of_mem (v : Vector α n) (ha' : a' ∈ v.toList) : a' ∈ (a ::ᵥ v).toList :=
  (Vector.mem_cons_iff a a' v).2 (Or.inr ha')

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

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

Разделы

Аффилиация

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