cons_val_succ' — Mathlib

English

For ⟨0, h⟩, vecCons x u ⟨0, h⟩ = x; the statement is the same as the previous case with explicit witness h.

Русский

Для ⟨0, h⟩, vecCons x u ⟨0, h⟩ = x; утверждение аналогично предыдущему случаю с явным доказательством h.

LaTeX

$$$\mathrm{vecCons} x u \langle 0, h \rangle = x$$$

Lean4

@[simp]
theorem cons_val_succ' {i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α) :
    vecCons x u ⟨i.succ, h⟩ = u ⟨i, Nat.lt_of_succ_lt_succ h⟩ := by simp only [vecCons, Fin.cons, Fin.cases_succ']

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