matrix_blockDiag' — Mathlib

English

If f sums to a, then blockDiag'(f) sums to blockDiag'(a).

Русский

Если f суммируется к a, то blockDiag'(f) суммируется к blockDiag'(a).

LaTeX

$$HasSum f a L ⇒ HasSum (λ x, blockDiagonal'(f x)) (blockDiagonal'(a)) L$$

Lean4

theorem matrix_blockDiag' {f : X → Matrix (Σ i, m' i) (Σ i, n' i) R} {a : Matrix (Σ i, m' i) (Σ i, n' i) R}
    (hf : HasSum f a L) : HasSum (fun x => blockDiag' (f x)) (blockDiag' a) L :=
  hf.map (blockDiag'AddMonoidHom m' n' R) continuous_id.matrix_blockDiag'

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