matrix_blockDiag' — Mathlib

English

For f : X → ∀ i, Matrix (m' i) (n' i) R, summability of blockDiagonal'(f) is equivalent to summability of f.

Русский

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

LaTeX

$$Summable f L ↔ Summable (λ x, blockDiagonal'(f x)) L$$

Lean4

theorem matrix_blockDiag' {f : X → Matrix (Σ i, m' i) (Σ i, n' i) R} (hf : Summable f L) :
    Summable (fun x => blockDiag' (f x)) L :=
  hf.hasSum.matrix_blockDiag'.summable

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