hasSum — Mathlib

English

Applying a continuous linear map commutes with taking an infinite sum: HasSum f x L implies HasSum (λ b, φ(f b)) (φ x) L.

Русский

Применение непрерывного линейного отображения commute со взятием бесконечной суммы: HasSum f x L ⇒ HasSum (λ b, φ(f b)) (φ x) L.

LaTeX

$$$$ \text{HasSum } f x L \Rightarrow \text{HasSum } (\lambda b, φ(f b)) (φ x) L. $$$$

Lean4

/-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
protected theorem hasSum {f : ι → M} (φ : M →SL[σ] M₂) {x : M} (hf : HasSum f x L) :
    HasSum (fun b : ι ↦ φ (f b)) (φ x) L := by simpa only using hf.map φ.toLinearMap.toAddMonoidHom φ.continuous

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