English
Applying a zero-preserving map to the entries of a block triangular matrix preserves block triangularity with the same labeling.
Русский
Применение отображения нулей к элементам блоково-треугольной матрицы сохраняет блочную треугольность при той же разметке.
LaTeX
$$$\BlockTriangular\, M\, b \Rightarrow \BlockTriangular\,(M.map\ f)\, b$$$
Lean4
theorem map {S F} [FunLike F R S] [Zero R] [Zero S] [ZeroHomClass F R S] (f : F) (h : BlockTriangular M b) :
BlockTriangular (M.map f) b := fun i j lt ↦ by simp [h lt]