cons_vec_bit0_eq_alt0 — Mathlib

English

The element at index i+i of vecCons x u equals the corresponding Alt0-construction of the repeated vector.

Русский

Элемент на позиции i+i в vecCons x u равен соответствующему Alt0-конструктору повторённого вектора.

LaTeX

$$$\\operatorname{vecCons} x u (i+i) = \\operatorname{vecAlt0}(⋯)(\\operatorname{vecAppend}(⋯)(\\operatorname{vecCons} x u)(\\operatorname{vecCons} x u))\,i$$$

Lean4

theorem cons_vec_bit0_eq_alt0 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
    vecCons x u (i + i) = vecAlt0 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i := by rw [vecAlt0_vecAppend]; rfl

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