comp — Mathlib

English

For matrices M block triangular with respect to b, the composition operation M.comp yields a block triangular matrix with blocks indexed by i ↦ b.i.1.

Русский

Для блочно-треугольной матрицы M по разметке b операция компоновки M.comp дает блочную треугольность с блоками, индексируемыми по i.1.

LaTeX

$$$\BlockTriangular\, M\; b \Rightarrow \BlockTriangular\bigl(M.comp\; m\; m\; n\; n\; R\bigr)\; (\lambda i. b(i).1)$$$

Lean4

theorem comp [Zero R] {M : Matrix m m (Matrix n n R)} (h : BlockTriangular M b) :
    BlockTriangular (M.comp m m n n R) fun i ↦ b i.1 := fun i j lt ↦ by simp [h lt]

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