toRows₁ — Mathlib

English

From a row-partitioned matrix A of size (m1 ⊕ m2) × n, extract the first row block as a matrix of size m1 × n by taking entries A(Sum.inl i, j).

Русский

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

LaTeX

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

Lean4

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

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