summable_imp_tendsto_iff_completeSpace

English

In a normed additive group, the statement that every absolutely convergent series converges is equivalent to the space being complete.

Русский

В нормированной аддитивной группе равносильно: каждая абсолютно сходящаяся по норме серия сходится тогда и только тогда, когда пространство полно.

LaTeX

$$$(\forall u:\mathbb{N}\to E,\ Summable(\|u\|) \Rightarrow \exists a, Tendsto(\lambda n. \sum_{i< n} u(i)) atTop (\mathcal{N}(a))) \iff \text{CompleteSpace}(E)$$$

Lean4

/-- In a normed additive group, every absolutely convergent series converges in the
space iff the space is complete. -/
theorem summable_imp_tendsto_iff_completeSpace :
    (∀ u : ℕ → E, Summable (‖u ·‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)) ↔ CompleteSpace E :=
  ⟨completeSpace_of_summable_imp_tendsto, fun _ u hu => summable_imp_tendsto_of_complete u hu⟩

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