English
If we form a matrix vecCons v B by inserting a top row vector v above a block B, then the i-th entry of the j-th column is given by the i-th entry of the concatenated column vecCons (v j) (·) applied to the j-th column of B; equivalently, the j-th column of vecCons v B is the column consisting of v j on top and the j-th column of B underneath.
Русский
Если получить матрицу vecCons v B, вставив сверху строковый вектор v над блоком B, то i-я запись j-го столбца равна i-й записи в столбце, полученном конкатенацией vecCons (v j) (·) над j-м столбцом B; иначе говоря, j-й столбец vecCons v B состоит из v_j сверху и столбца B под ним.
LaTeX
$$$(\\mathrm{vecCons}\\, v\\, B)_{i j} = \\bigl( \\mathrm{vecCons}(v j) (\\lambda i, B i j) \\bigr)_i$$$
Lean4
@[simp]
theorem cons_val' (v : n' → α) (B : Fin m → n' → α) (i j) : vecCons v B i j = vecCons (v j) (fun i => B i j) i := by
refine Fin.cases ?_ ?_ i <;> simp
