submatrix_cons_row — Mathlib

English

Let A be a matrix. Then the submatrix with an added top row i and following rows row equals vecCons (fun j => A i (col j)) (A.submatrix row col).

Русский

Пусть A — матрица. Подматрица с добавленной сверху строкой i и оставшимися строками row равна vecCons (функция j ↦ A(i, col j)) (A.submatrix row col).

LaTeX

$$$A.submatrix(\mathrm{vecCons}(i,row), col) = \mathrm{vecCons}(\lambda j. A(i, col(j))),\; A.submatrix(row,col).$$$

Lean4

@[simp]
theorem submatrix_cons_row (A : Matrix m' n' α) (i : m') (row : Fin m → m') (col : o' → n') :
    submatrix A (vecCons i row) col = vecCons (fun j => A i (col j)) (submatrix A row col) :=
  by
  ext i j
  refine Fin.cases ?_ ?_ i <;> simp [submatrix]

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