summable — Mathlib

English

If φ is a continuous semilinear map from M to M₂ and f: ι → M is summable (with respect to L), then the transformed family b ↦ φ(f(b)) is also summable (with respect to L).

Русский

Пусть φ — непрерывное полинормированное отображение из M в M₂, и пусть f: ι → M суммируемо относительно фильтра L; тогда последовательность φ(f(i)) суммируема относительно L.

LaTeX

$$$\\forall f:\\, ι \\to M,\\; \\mathrm{Summable}(f,L) \\Rightarrow \\mathrm{Summable}(\\lambda b:ι,\\, \\phi(f(b)),L)$$$

Lean4

protected theorem summable {f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f L) : Summable (fun b : ι ↦ φ (f b)) L :=
  (hf.hasSum.mapL φ).summable

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