vecAppend_apply_zero — Mathlib

English

If o + 1 = m + 1 + n and u has length m + 1 while v has length n, then the 0-th entry of vecAppend ho u v equals the 0-th entry of u.

Русский

Если o+1 = m+1+n и длина u равна m+1, а длина v равна n, то нулевой элемент vecAppend ho u v равен нулевому элементу u.

LaTeX

$$$\\vecAppend(ho,u,v)(0) = u(0)$$$

Lean4

@[simp]
theorem vecAppend_apply_zero {α : Type*} {o : ℕ} (ho : o + 1 = m + 1 + n) (u : Fin (m + 1) → α) (v : Fin n → α) :
    vecAppend ho u v 0 = u 0 :=
  dif_pos _

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