get_mem

Mathlib.Data.Vector.Mem

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

English

For any i ∈ Fin n and any vector v ∈ Vector α n, the value v.get i is a member of the list v.toList.

Русский

Для любого i ∈ Fin n и вектора v ∈ Vector α n значение v.get i принадлежит списку v.toList.

LaTeX

$$$$ v.get(i) \in v.toList $$$$

Lean4

@[simp]
theorem get_mem (i : Fin n) (v : Vector α n) : v.get i ∈ v.toList :=
  List.get_mem _ _

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

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

Разделы

Аффилиация

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