cons_head_tail

Mathlib.Data.Fin.VecNotation

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

English

A vector constructed from the head and tail of a vector recovers the original vector.

Русский

Вектор, построенный из головы и хвоста вектора, восстанавливает исходный вектор.

LaTeX

$$$\mathrm{vecCons}(\mathrm{vecHead}~u, \mathrm{vecTail}~u) = u$$$

Lean4

@[simp]
theorem cons_head_tail (u : Fin m.succ → α) : vecCons (vecHead u) (vecTail u) = u :=
  Fin.cons_self_tail _

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

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

Разделы

Аффилиация

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