mathlib documentation

topology.​metric_space.​cau_seq_filter

topology.​metric_space.​cau_seq_filter

Completeness in terms of cauchy filters vs is_cau_seq sequences

In this file we apply metric.complete_of_cauchy_seq_tendsto to prove that a normed_ring is complete in terms of cauchy filter if and only if it is complete in terms of cau_seq Cauchy sequences.

theorem cauchy_seq.​is_cau_seq {β : Type v} [normed_field β] {f : → β} :

theorem cau_seq.​cauchy_seq {β : Type v} [normed_field β] (f : cau_seq β has_norm.norm) :

theorem cau_seq_iff_cauchy_seq {α : Type u} [normed_field α] {u : → α} :

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

@[instance]

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

Equations