submatrix_updateCol_succAbove — Mathlib

English

Updating a column and then taking the submatrix above the updated index is the same as directly taking the submatrix above the index.

Русский

Обновление столбца и последующее взятие подматрицы над обновлённой позицией равно взятию подматрицы над соответствующей позицией без обновления.

LaTeX

$$$\big(A.updateCol(i,v)\big).submatrix(f,i.succAbove) = A.submatrix(f,i.succAbove)$$$

Lean4

/-- Updating a column then removing it is the same as removing it. -/
@[simp]
theorem submatrix_updateCol_succAbove (A : Matrix m' (Fin n.succ) α) (v : m' → α) (f : o' → m') (i : Fin n.succ) :
    (A.updateCol i v).submatrix f i.succAbove = A.submatrix f i.succAbove :=
  ext fun _r s => updateCol_ne (Fin.succAbove_ne i s)

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