English
ToBlock M p q is the block matrix obtained from M by selecting rows with property p and columns with property q; its entries are given by M restricted to those indices.
Русский
ToBlock M p q — это блоковая матрица, полученная из M путём выбора строк с условием p и столбцов с условием q; её элементы — это значения M на соответствующих индексах.
LaTeX
$$$ \\text{toBlock } M\\; p\\; q : \\text{Matrix} \\{a // p a\\} \\{b // q b\\} \\alpha \\\\ (\\text{toBlock } M\\; p\\; q)_{i j} = M_{i,j} $$$
Lean4
/-- Let `p` pick out certain rows and `q` pick out certain columns of a matrix `M`. Then
`toBlock M p q` is the corresponding block matrix. -/
def toBlock (M : Matrix m n α) (p : m → Prop) (q : n → Prop) : Matrix { a // p a } { a // q a } α :=
M.submatrix (↑) (↑)
