English
From blocks of a matrix with sum-type indices, we can extract the corresponding top-left, top-right, bottom-left, and bottom-right submatrices as blocks of the original matrix.
Русский
Из блоков матрицы с индексами, являющимися суммой типов, можно извлечь соответствующие подматрицы: верхний левый, верхний правый, нижний левый и нижний правый блоки.
LaTeX
$$$ (\text{fromBlocks } A B C D).toBlocks_{11} = A,\quad (\text{fromBlocks } A B C D).toBlocks_{12} = B,\quad (\text{fromBlocks } A B C D).toBlocks_{21} = C,\quad (\text{fromBlocks } A B C D).toBlocks_{22} = D $$$
Lean4
/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
"top right" submatrix. -/
def toBlocks₁₂ (M : Matrix (n ⊕ o) (l ⊕ m) α) : Matrix n m α :=
of fun i j => M (Sum.inl i) (Sum.inr j)
