hasSum_snd — Mathlib

English

If f is a summable family in tsze R M with sum a, then the snd-projection has sum snd(a).

Русский

Если f — суммабельная в tsze R M с суммой a, то сумма по второй координате равна snd(a).

LaTeX

$$$\\forall {f : \\alpha \\to tsze(R,M)} {a : tsze(R,M)},\\ HasSum f a \\Rightarrow HasSum (\\lambda x, \\mathrm{snd}(f x)) (\\mathrm{snd}(a))$$$

Lean4

theorem hasSum_snd [AddCommMonoid R] [AddCommMonoid M] {f : α → tsze R M} {a : tsze R M} (h : HasSum f a) :
    HasSum (fun x ↦ snd (f x)) (snd a) :=
  h.map (⟨⟨snd, snd_zero⟩, snd_add⟩ : tsze R M →+ M) continuous_snd

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