summable — Mathlib

English

A continuous linear map preserves tsum of a sequence, i.e., tsum of the mapped sequence equals the mapped tsum.

Русский

Непрерывно-линейное отображение сохраняет сумму: tsum(φ ∘ f) = φ(tsum f).

LaTeX

$$$\\forall f:\\, ι \\to M\\ (hf: Summable f L),\\; φ(\\operatorname{tsum}_L f) = \\operatorname{tsum}_L (λ z, φ(f(z)))$$$

Lean4

protected theorem summable {f : ι → M} (e : M ≃SL[σ] M₂) : (Summable (fun b : ι ↦ e (f b)) L) ↔ Summable f L :=
  ⟨fun hf ↦ (e.hasSum.1 hf.hasSum).summable, (e : M →SL[σ] M₂).summable⟩

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