English
If f is Summable, then blockDiagonal'(f) is Summable.
Русский
Если f суммируема, то blockDiagonal'(f) суммируема.
LaTeX
$$Summable f L ⇒ Summable (λ x, blockDiagonal'(f x)) L$$
Lean4
theorem summable_matrix_blockDiagonal' [DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R} :
(Summable (fun x => blockDiagonal' (f x)) L) ↔ Summable f L :=
Summable.map_iff_of_leftInverse (blockDiagonal'AddMonoidHom m' n' R) (blockDiag'AddMonoidHom m' n' R)
continuous_id.matrix_blockDiagonal' continuous_id.matrix_blockDiag' fun A => blockDiag'_blockDiagonal' A