toCols₁ — Mathlib

English

From a column-partitioned matrix A of size m × (n1 ⊕ n2), extract the first block column as a matrix of size m × n1 by taking entries A(i, Sum.inl j).

Русский

Из колоночной разбиённой матрицы A размера m × (n1 ⊕ n2) извлекаем первый блоковый столбец размера m × n1, беря элементы A(i, Sum.inl j).

LaTeX

$$$\\text{toCols₁}(A)_{i j} = A_{i,(\\text{Sum.inl } j)}$$$

Lean4

/-- Given a column partitioned matrix extract the first column -/
def toCols₁ (A : Matrix m (n₁ ⊕ n₂) R) : Matrix m n₁ R :=
  of fun i j => (A i (Sum.inl j))

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