cons_val_one — Mathlib

English

For any x and u, vecCons x u 1 equals u 0; the second element is the first of u.

Русский

Для любых x и u, vecCons x u 1 равно u 0; второй элемент — первый элемент u.

LaTeX

$$$\mathrm{vecCons} x u 1 = u 0$$$

Lean4

/-- `![a, b, ...] 1` is equal to `b`.

  The simplifier needs a special lemma for length `≥ 2`, in addition to
  `cons_val_succ`, because `1 : Fin 1 = 0 : Fin 1`.
-/
@[simp]
theorem cons_val_one (x : α) (u : Fin m.succ → α) : vecCons x u 1 = u 0 :=
  rfl

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