blockDiagonal'_tsum — Mathlib

English

The sum of blockDiagonal' equals the blockDiagonal' of tsum.

Русский

Сумма по blockDiagonal' равна blockDiagonal'(сумме).

LaTeX

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

Lean4

theorem blockDiagonal'_tsum [DecidableEq l] [T2Space R] {f : X → ∀ i, Matrix (m' i) (n' i) R} :
    blockDiagonal' (∑'[L] x, f x) = ∑'[L] x, blockDiagonal' (f x) :=
  Function.LeftInverse.map_tsum (g := blockDiagonal'AddMonoidHom m' n' R) f continuous_id.matrix_blockDiagonal'
    continuous_id.matrix_blockDiag' blockDiag'_blockDiagonal'

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