blockTriangular_diagonal — Mathlib

English

The diagonal matrix diag(d) is block triangular with respect to any labeling b, for suitable d.

Русский

Диагональная матрица diag(d) блочно-треугольна по любой разметке b.

LaTeX

$$$\BlockTriangular\bigl(\mathrm{diagonal}(d)\bigr)\; b$$$

Lean4

theorem blockTriangular_diagonal [DecidableEq m] (d : m → R) : BlockTriangular (diagonal d) b := fun _ _ h =>
  diagonal_apply_ne' d fun h' => ne_of_lt h (congr_arg _ h')

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