get_append_cons_succ — Mathlib

English

For any index i in Fin(n+m) (represented as i with a successor form), the element at position i+1 in (x :: xs) ++ ys is the element at position i in xs ++ ys.

Русский

Для любого индекса i в Fin(n+m) элемент на позиции i+1 в (x :: xs) ++ ys равен элементу на позиции i в xs ++ ys.

LaTeX

$$$\\mathrm{get}((x \\;::ᵥ\\; xs) \\;++\\; ys)\\;\\langle i+1, h \\rangle = \\mathrm{get} (xs \\;++\\; ys)\\; i$$$

Lean4

@[simp]
theorem get_append_cons_succ {i : Fin (n + m)} {h} : get (x ::ᵥ xs ++ ys) ⟨i + 1, h⟩ = get (xs ++ ys) i :=
  rfl

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