summable_matrix_blockDiagonal' — Mathlib

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

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