hasSum_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem hasSum_inr [AddCommMonoid R] [AddCommMonoid M] {f : α → M} {a : M} (h : HasSum f a) :
    HasSum (fun x ↦ inr (f x)) (inr a : tsze R M) :=
  h.map (⟨⟨inr, inr_zero _⟩, inr_add _⟩ : M →+ tsze R M) continuous_inr

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