submatrix — Mathlib

English

If M is block triangular with respect to b, then any submatrix obtained by restricting both rows and columns via a map f : n → m is block triangular with respect to the composed labeling b ∘ f.

Русский

Если матрица M блочно-треугольная по отношению к разметке b, то любая подматрица, полученная ограничением по строкам и столбцам через отображение f: n → m, снова блочно-треугольна по разметке b ∘ f.

LaTeX

$$$\BlockTriangular M\; b \Rightarrow \BlockTriangular\bigl(M.submatrix\;f\;f\bigr) (b \circ f)$$$

Lean4

@[simp]
protected theorem submatrix {f : n → m} (h : M.BlockTriangular b) : (M.submatrix f f).BlockTriangular (b ∘ f) :=
  fun _ _ hij => h hij

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