toBlock_apply — Mathlib

English

Applying toBlock to M with predicates p and q yields a matrix whose (i,j) entry is M(i.val, j.val).

Русский

Применение toBlock к M с предикатами p и q даёт матрицу, у которой элемент (i,j) равен M(i.val, j.val).

LaTeX

$$$ \\text{toBlock } M\\; p\\; q\\; i\\; j = M_{i.\\mathrm{val}, j.\\mathrm{val}} $$$

Lean4

@[simp]
theorem toBlock_apply (M : Matrix m n α) (p : m → Prop) (q : n → Prop) (i : { a // p a }) (j : { a // q a }) :
    toBlock M p q i j = M ↑i ↑j :=
  rfl

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