cons_val_two

Mathlib.Data.Fin.VecNotation

URI: https://scilib.ai/kg/mathlib#Matrix.cons_val_two

English

The value at index 2 of vecCons x u is the head of the tail of u.

Русский

Значение на индексе 2 vecCons x u равно голове хвоста u.

LaTeX

$$$\mathrm{vecCons} x u 2 = \mathrm{vecHead}(\mathrm{vecTail} u)$$$

Lean4

theorem cons_val_two (x : α) (u : Fin m.succ.succ → α) : vecCons x u 2 = vecHead (vecTail u) :=
  rfl

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

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

Разделы

Аффилиация

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