toSquareBlock_def — Mathlib

English

The block for a given map b and value k is the matrix whose entries are M(i,j) with i and j restricted to the subset where b(i) = k and b(j) = k.

Русский

Блок для заданной карты b и значения k — это матрица, элементы которой равны M(i,j) при ограничении i и j на подмножество { a | b(a)=k }.

LaTeX

$$$ \\text{toSquareBlock }(M,b,k) = \\mathrm{of} \\bigl( \\lambda i j : \\{ a // b a = k \\}, M(i.val, j.val) \\bigr) $$$

Lean4

theorem toSquareBlock_def (M : Matrix m m α) (b : m → β) (k : β) :
    toSquareBlock M b k = of (fun i j : { a // b a = k } => M ↑i ↑j) :=
  rfl

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