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) : CauchySeq ↑f

theorem isCauSeq_iff_cauchySeq {α : Type u} [NormedField α] {u : ℕ → α} : IsCauSeq norm u ↔ CauchySeq u

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

@[instance 100]

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

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

Equations

• ⋯ = ⋯