hasSum_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem hasSum_fst [AddCommMonoid R] [AddCommMonoid M] {f : α → tsze R M} {a : tsze R M} (h : HasSum f a) :
    HasSum (fun x ↦ fst (f x)) (fst a) :=
  h.map (⟨⟨fst, fst_zero⟩, fst_add⟩ : tsze R M →+ R) continuous_fst

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