hasSum' — Mathlib

English

Applying a continuous linear equivalence to a summable family preserves summation, i.e., hasSum equivalence with the inverse map.

Русский

Применение непрерывного линейного эквивалента к суммируемой семье сохраняет суммирование; эквивалентность по сумме через обратную карту.

LaTeX

$$$\\forall f:\\, ι \\to M,\\; (HasSum (\\lambda i, e(f(i))) (e(x)) L) \\Leftrightarrow HasSum f x L$$$

Lean4

/-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
protected theorem hasSum' {f : ι → M} (e : M ≃SL[σ] M₂) {x : M} : HasSum (fun b : ι ↦ e (f b)) (e x) L ↔ HasSum f x L :=
  by rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]

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