summable_matrix_blockDiagonal — Mathlib

English

For f : X → p → Matrix m×n R, summability of blockDiagonal(f) is equivalent to summability of f.

Русский

Для f: X → p → Matrix m×n R суммируемость blockDiagonal(f) эквивалентна суммируемости f.

LaTeX

$$Summable((λ x, Matrix.blockDiagonal (f x)), L) ↔ Summable(f, L)$$

Lean4

theorem summable_matrix_blockDiagonal [DecidableEq p] {f : X → p → Matrix m n R} :
    (Summable (fun x => blockDiagonal (f x)) L) ↔ Summable f L :=
  Summable.map_iff_of_leftInverse (blockDiagonalAddMonoidHom m n p R) (blockDiagAddMonoidHom m n p R)
    continuous_id.matrix_blockDiagonal continuous_id.matrix_blockDiag fun A => blockDiag_blockDiagonal A

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