matrix_blockDiagonal

Mathlib.Topology.Instances.Matrix

URI: https://scilib.ai/kg/mathlib#Summable.matrix_blockDiagonal

← MathLib Explorer

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 matrix_blockDiagonal [DecidableEq p] {f : X → p → Matrix m n R} (hf : Summable f L) :
    Summable (fun x => blockDiagonal (f x)) L :=
  hf.hasSum.matrix_blockDiagonal.summable

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru