cons_val_three

Mathlib.Data.Fin.VecNotation

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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