append_right — Mathlib

English

For u : Fin m → α, v : Fin n → α, and i : Fin n, the right part of the appended sequence matches v: append u v (natAdd m i) = v i.

Русский

Для u: Fin m → α, v: Fin n → α и i ∈ Fin n, правая часть дописываемой последовательности равна v(i): append u v (natAdd m i) = v i.

LaTeX

$$$\\mathrm{append}(u,v)(\\mathrm{natAdd}\\ m\\ i) = v(i).$$$

Lean4

@[simp]
theorem append_right (u : Fin m → α) (v : Fin n → α) (i : Fin n) : append u v (natAdd m i) = v i :=
  addCases_right _

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