sub — Mathlib

English

The difference of two block triangular matrices with the same labeling is block triangular with respect to that labeling.

Русский

Разность двух блочно-треугольных матриц по одной и той же разметке сохраняет блочную треугольность.

LaTeX

$$$\BlockTriangular\, M\; b \land \BlockTriangular\, N\; b \Rightarrow \BlockTriangular\,(M-N)\; b$$$

Lean4

theorem sub [SubNegZeroMonoid R] (hM : BlockTriangular M b) (hN : BlockTriangular N b) : BlockTriangular (M - N) b :=
  fun i j h => by simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]

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