cons_vecAlt1 — Mathlib

English

vecAlt1 distributes over vecCons similarly to Alt0 with the right offset.

Русский

vecAlt1 распределяется по vecCons аналогично Alt0, с учётом смещения.

LaTeX

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

Lean4

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

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