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 f.lim)
theorem CauchySeq.isCauSeq {β : Type v} [NormedField β] {f : β} (hf : CauchySeq f) :
IsCauSeq norm f
theorem CauSeq.cauchySeq {β : Type v} [NormedField β] (f : CauSeq β norm) :
theorem isCauSeq_iff_cauchySeq {α : Type u} [NormedField α] {u : α} :

In a normed field, CauSeq coincides with the usual notion of Cauchy sequences.

@[instance 100]

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

  • =