BlockTriangular — Mathlib

English

Block triangularity: given a matrix M and a map b from indices to blocks, M is BlockTriangular if entries below different blocks follow the inequality b j < b i implies M i j = 0.

Русский

Блочное треугольное разложение: для матрицы M и отображения b: i ↦ блоки, если j блок меньше i, то M_{i j} = 0.

LaTeX

$$$$\text{BlockTriangular}(M, b) := \forall \; i,j, \; b(j) < b(i) \Rightarrow M_{ij} = 0.$$$$

Lean4

/-- Let `b` map rows and columns of a square matrix `M` to blocks indexed by `α`s. Then
`BlockTriangular M n b` says the matrix is block triangular. -/
def BlockTriangular (M : Matrix m m R) (b : m → α) : Prop :=
  ∀ ⦃i j⦄, b j < b i → M i j = 0

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