map_tsum — Mathlib

English

A continuous linear equivalence interchanges the infinite sum with the map: φ( tsum_L f ) = tsum_L (φ ∘ f).

Русский

Пусть e — непрерывное линейное эквивалентно между M и M₂; тогда e(tsum_L f) = tsum_L (e ∘ f).

LaTeX

$$$\\forall f:\\, ι \\to M,\\; \\mathrm{Summable}(f,L) \\Rightarrow \\phi(\\operatorname{tsum}_L f) = \\operatorname{tsum}_L (\\lambda z, \\phi(f(z)))$$$

Lean4

protected theorem map_tsum [T2Space M₂] [L.NeBot] {f : ι → M} (φ : M →SL[σ] M₂) (hf : Summable f L) :
    φ (∑'[L] z, f z) = ∑'[L] z, φ (f z) :=
  (hf.hasSum.mapL φ).tsum_eq.symm

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