toCols₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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