cons_vecAlt0 — Mathlib

English

vecAlt0 distributes over vecCons: combining x with u inside vecAlt0 corresponds to placing x and then recursing on u.

Русский

vecAlt0 распространяется на vecCons: вставка x и далее рекурсивная обработка u.

LaTeX

$$$\\text{vecAlt0}(h)(\\text{vecCons }x u) = \\text{vecCons }x (\\text{vecAlt0}(by cutsat)\\, u)$$$

Lean4

@[simp]
theorem cons_vecAlt0 (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
    vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 (by cutsat) u) :=
  by
  ext i
  simp_rw [vecAlt0]
  rcases i with ⟨⟨⟩ | i, hi⟩
  · rfl
  · simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ', vecAlt0]

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