Skip to content

Commit

Permalink
chore(topology/algebra/infinite_sum): reference Cauchy criterion in d…
Browse files Browse the repository at this point in the history
…ocs (#12172)
  • Loading branch information
ecstatic-morse committed Feb 21, 2022
1 parent 634dfc8 commit 3ad7395
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/topology/algebra/infinite_sum.lean
Expand Up @@ -1022,6 +1022,7 @@ section uniform_group

variables [add_comm_group α] [uniform_space α]

/-- The **Cauchy criterion** for infinite sums, also known as the **Cauchy convergence test** -/
lemma summable_iff_cauchy_seq_finset [complete_space α] {f : β → α} :
summable f ↔ cauchy_seq (λ (s : finset β), ∑ b in s, f b) :=
cauchy_map_iff_exists_tendsto.symm
Expand Down

0 comments on commit 3ad7395

Please sign in to comment.