English
If e: M ≃SL[σ] M₂ is a continuous linear equivalence, then HasSum of the transformed sequence e(f(i)) to y is equivalent to HasSum of f to e⁻¹(y).
Русский
Если e: M ≃SL[σ] M₂ — непрерывное линейное эквивалентное отображение, то HasSum (e(f(i))) к y эквивалентно HasSum f к e.symm(y).
LaTeX
$$$\\forall f:\\, ι \\to M,\\; (\\exists y:\\, M₂,\\ HasSum (\\lambda i, e(f(i)))\\, y \\Leftrightarrow HasSum f (e^{-1}(y)))$$$
Lean4
/-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
protected theorem hasSum {f : ι → M} (e : M ≃SL[σ] M₂) {y : M₂} :
HasSum (fun b : ι ↦ e (f b)) y L ↔ HasSum f (e.symm y) L :=
⟨fun h ↦ by simpa only [e.symm.coe_coe, e.symm_apply_apply] using h.mapL (e.symm : M₂ →SL[σ'] M), fun h ↦ by
simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h⟩
