English
For B as above and fixed j, the tail of the column given by B equals the column formed by taking the tails of B entrywise, i.e., the tail of the j-th column is vecTail B i j as a function of i.
Русский
Для данного B и фиксированного j хвост столбца равен столбцу, составленному из хвостов B по строкам: хвост j-го столбца равен vecTail B i j как функция от i.
LaTeX
$$$\\mathrm{vecTail}( \\lambda i. B i j ) = \\lambda i. \\mathrm{vecTail} B i j$$$
Lean4
@[simp]
theorem tail_val' (B : Fin m.succ → n' → α) (j : n') : (vecTail fun i => B i j) = fun i => vecTail B i j :=
rfl