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 matrix_blockDiagonal' [DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R} {a : ∀ i, Matrix (m' i) (n' i) R}
    (hf : HasSum f a L) : HasSum (fun x => blockDiagonal' (f x)) (blockDiagonal' a) L :=
  hf.map (blockDiagonal'AddMonoidHom m' n' R) continuous_id.matrix_blockDiagonal'

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