mem_cons_self

Mathlib.Data.Vector.Mem

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

English

The element a is a member of the list corresponding to (a ::ᵥ v).

Русский

Элемент a принадлежит списку, соответствующему (a ::ᵥ v).

LaTeX

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

Lean4

theorem mem_cons_self (v : Vector α n) : a ∈ (a ::ᵥ v).toList :=
  (Vector.mem_iff_get a (a ::ᵥ v)).2 ⟨0, Vector.get_cons_zero a v⟩

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

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

Разделы

Аффилиация

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