cons_val_four — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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