append_left — Mathlib

English

For u : Fin m → α, v : Fin n → α, and i : Fin m, the left part of the appended sequence is preserved: append u v (Fin.castAdd n i) = u i.

Русский

Пусть u: Fin m → α, v: Fin n → α, i: Fin m. Тогда элемент слева от добавления сохраняется: append u v (Fin.castAdd n i) = u i.

LaTeX

$$$\\mathrm{append}(u,v)(\\mathrm{Fin.castAdd}\\ n\\ i) = u(i).$$$

Lean4

@[simp]
theorem append_left (u : Fin m → α) (v : Fin n → α) (i : Fin m) : append u v (Fin.castAdd n i) = u i :=
  addCases_left _

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