hasSum_inl — Mathlib

English

If f is a summable family in R with sum a, then the family x ↦ inl(f x) has sum inl(a) in tsze R M.

Русский

Если f — суммабельная семья в R с суммой a, то семья x ↦ inl(f x) имеет сумму inl(a) в tsze R M.

LaTeX

$$$\\forall [AddCommMonoid R] [AddCommMonoid M],\\ HasSum f a \\Rightarrow HasSum (x \\mapsto \\mathrm{inl}(f x)) (\\mathrm{inl}(a))$$$

Lean4

theorem hasSum_inl [AddCommMonoid R] [AddCommMonoid M] {f : α → R} {a : R} (h : HasSum f a) :
    HasSum (fun x ↦ inl (f x)) (inl a : tsze R M) :=
  h.map (⟨⟨inl, inl_zero _⟩, inl_add _⟩ : R →+ tsze R M) continuous_inl

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