English
Let A be m × n, j : n, c : m → α, e : l ≃ m, f : o ≃ n. Then (A.updateCol j c).submatrix e f equals updateCol of the submatrix A.submatrix e f at f.symm j with c transported via e: (A.updateCol j c).submatrix e f = updateCol (A.submatrix e f) (f.symm j) (λ i, c (e i)).
Русский
Пусть A — матрица размером m×n, j : n, c : m → α, e : l ≃ m, f : o ≃ n. Тогда (A.updateCol j c).submatrix e f равно обновлению столбца подматрицы A.submatrix e f в позиции f.symm j с переносом c через e: (A.updateCol j c).submatrix e f = updateCol (A.submatrix e f) (f.symm j) (λ i, c (e i)).
LaTeX
$$$$ (A.updateCol j c).submatrix e f = updateCol (A.submatrix e f) (f.symm j) (\lambda i, c (e i)) $$$$
Lean4
theorem submatrix_updateCol_equiv [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : l ≃ m)
(f : o ≃ n) : (A.updateCol j c).submatrix e f = updateCol (A.submatrix e f) (f.symm j) fun i => c (e i) :=
Eq.trans (by simp_rw [Equiv.apply_symm_apply]) (updateCol_submatrix_equiv A _ _ e f).symm
