summable_iff_summable_compl_and_tsum_mem

English

If f is summable, then the sum in the completion equals the completion of the sum.

Русский

Если f суммируемо, то сумма в дополнении равна образу суммы в дополнении.

LaTeX

$$$$ ∑'[L] i, toCompl (f i) = toCompl\left( ∑'[L] i, f i \right). $$$$

Lean4

/-- A function `f` is summable in a uniform additive group `α` if and only if it is summable in
`Completion α` and its sum in `Completion α` lies in the range of `toCompl : α →+ Completion α`. -/
theorem summable_iff_summable_compl_and_tsum_mem (f : β → α) :
    Summable f L ↔ Summable (toCompl ∘ f) L ∧ ∑'[L] i, toCompl (f i) ∈ Set.range toCompl :=
  (isDenseInducing_toCompl α).summable_iff_tsum_comp_mem_range f

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