toSquareBlock — Mathlib

English

For a square matrix M, and a map b: m → β and an index k ∈ β, toSquareBlock M b k is the block with indices where b a = k.

Русский

Для квадратной матрицы M и отображения b: m → β, индекса k ∈ β, toSquareBlock M b k — это блок с индексами, для которых b(a) = k.

LaTeX

$$$ \\text{toSquareBlock }(M,b,k) = \\text{toSquareBlockProp }(M, \\lambda a . b(a) = k) $$$

Lean4

/-- Let `b` map rows and columns of a square matrix `M` to blocks. Then
  `toSquareBlock M b k` is the block `k` matrix. -/
def toSquareBlock (M : Matrix m m α) (b : m → β) (k : β) : Matrix { a // b a = k } { a // b a = k } α :=
  toSquareBlockProp M _

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