map — Mathlib

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]

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