English
Let A be an m × (n1+n2) matrix. Let A_left be its left block of size m × n1 and A_right its right block of size m × n2. Then A equals the concatenation fromCols(A_left, A_right). In particular, A = fromCols(A.toCols₁, A.toCols₂).
Русский
Пусть A — матрица размерности m × (n1+n2). Пусть A_L — её левая часть размерности m × n1, A_R — правая часть размерности m × n2. Тогда A = fromCols(A_L, A_R). В частности, A = fromCols(A.toCols₁, A.toCols₂).
LaTeX
$$$$A = \operatorname{fromCols}(A_{\text{left}}, A_{\text{right}})\quad\text{with }A_{\text{left}} = A^{\text{left}},\ A_{\text{right}} = A^{\text{right}}.$$$$
Lean4
@[simp]
theorem fromCols_toCols (A : Matrix m (n₁ ⊕ n₂) R) : fromCols A.toCols₁ A.toCols₂ = A := by ext i (j | j) <;> simp
