get_cons_zero

Mathlib.Data.Vector.Basic

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

English

The zeroth element of a vector formed by prepending a to an existing vector v is a.

Русский

Нулевой элемент вектора, полученного добавлением элемента a спереди к v, равен a.

LaTeX

$$$\\forall {\\alpha} (a:\\alpha) (v:\\mathrm{Vector}\\ \\alpha\\ n),\\; \\mathrm{get}(\\mathrm{cons}(a,v),0) = a$$$

Lean4

theorem get_cons_zero (a : α) (v : Vector α n) : get (a ::ᵥ v) 0 = a := by simp [get_zero]

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

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

Разделы

Аффилиация

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