add — Mathlib

English

The sum 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 add [AddZeroClass R] (hM : BlockTriangular M b) (hN : BlockTriangular N b) : BlockTriangular (M + N) b :=
  fun i j h => by simp_rw [Matrix.add_apply, hM h, hN h, zero_add]

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