blockTriangular_blockDiagonal' — Mathlib

English

For a family d : α → Matrix (m' i) (m' i) R, the blockDiagonal' d is block triangular with respect to Prod.fst.

Русский

Для семейства матриц d(i) матрица blockDiagonal' d блочно-треугольна по Prod.fst.

LaTeX

$$$\BlockTriangular\bigl(\mathrm{blockDiagonal}'\; d\bigr)\; \Sigma.fst$$$

Lean4

theorem blockTriangular_blockDiagonal' [DecidableEq α] (d : ∀ i : α, Matrix (m' i) (m' i) R) :
    BlockTriangular (blockDiagonal' d) Sigma.fst :=
  by
  rintro ⟨i, i'⟩ ⟨j, j'⟩ h
  apply blockDiagonal'_apply_ne d i' j' fun h' => ne_of_lt h h'.symm

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