matrix_diagonal — Mathlib

English

Let L be a summation filter on X and f: X → n → R. If f is Summable with respect to L, then the map x ↦ diag(f(x)) is Summable with respect to L.

Русский

Пусть L — фильтр суммирования на X и f: X → n → R. Если f суммируема по L, то отображение x ↦ diag(f(x)) суммируемо по L.

LaTeX

$$$\mathrm{Summable}(f,L) \Rightarrow \mathrm{Summable}(x \mapsto \operatorname{diag}(f(x)),L)$$$

Lean4

theorem matrix_diagonal [DecidableEq n] {f : X → n → R} (hf : Summable f L) : Summable (fun x => diagonal (f x)) L :=
  hf.hasSum.matrix_diagonal.summable

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