# Completeness in terms of `Cauchy`

filters vs `isCauSeq`

sequences #

In this file we apply `Metric.complete_of_cauchySeq_tendsto`

to prove that a `NormedRing`

is complete in terms of `Cauchy`

filter if and only if it is complete in terms
of `CauSeq`

Cauchy sequences.

theorem
CauSeq.tendsto_limit
{β : Type v}
[NormedRing β]
[hn : IsAbsoluteValue norm]
(f : CauSeq β norm)
[CauSeq.IsComplete β norm]
:

Filter.Tendsto (↑f) Filter.atTop (nhds (CauSeq.lim f))

theorem
CauchySeq.isCauSeq
{β : Type v}
[NormedField β]
{f : ℕ → β}
(hf : CauchySeq f)
:

IsCauSeq norm f

In a normed field, `CauSeq`

coincides with the usual notion of Cauchy sequences.

instance
completeSpace_of_cauSeq_isComplete
{β : Type v}
[NormedField β]
[CauSeq.IsComplete β norm]
:

A complete normed field is complete as a metric space, as Cauchy sequences converge by assumption and this suffices to characterize completeness.