cons_vec_bit1_eq_alt1 — Mathlib

English

Analogous equality holds for bit1 and Alt1 construction.

Русский

Аналогично выполняется равенство для бит1 и конструктора Alt1.

LaTeX

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

Lean4

theorem cons_vec_bit1_eq_alt1 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
    vecCons x u ((i + i) + 1) = vecAlt1 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i := by rw [vecAlt1_vecAppend];
  rfl

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