blockDiagonal_tsum — Mathlib

English

The sum over a blockDiagonal of a family equals the blockDiagonal of the sum: blockDiagonal (tsum f) = tsum (blockDiagonal f).

Русский

Сумма по блочной диагонали равна блочной диагонали суммы: blockDiagonal(tsum f) = tsum(blockDiagonal f).

LaTeX

$$blockDiagonal (tsum(f,L)) = tsum(λ x, blockDiagonal (f x), L)$$

Lean4

theorem blockDiagonal_tsum [DecidableEq p] [T2Space R] {f : X → p → Matrix m n R} :
    blockDiagonal (∑'[L] x, f x) = ∑'[L] x, blockDiagonal (f x) :=
  Function.LeftInverse.map_tsum (g := blockDiagonalAddMonoidHom m n p R) f continuous_id.matrix_blockDiagonal
    continuous_id.matrix_blockDiag blockDiag_blockDiagonal

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