mathlib3 documentation

topology.metric_space.cau_seq_filter

Completeness in terms of cauchy filters vs is_cau_seq sequences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
theorem cau_seq.tendsto_limit {β : Type v} [normed_ring β] [hn : is_absolute_value has_norm.norm] (f : cau_seq β has_norm.norm) [cau_seq.is_complete β has_norm.norm] :
filter.tendsto ⇑f filter.at_top (nhds f.lim)
source
theorem cauchy_seq.is_cau_seq {β : Type v} [normed_field β] {f : ℕ → β} (hf : cauchy_seq f) :
is_cau_seq has_norm.norm f
source
theorem cau_seq.cauchy_seq {β : Type v} [normed_field β] (f : cau_seq β has_norm.norm) :
cauchy_seq ⇑f
source
theorem cau_seq_iff_cauchy_seq {α : Type u} [normed_field α] {u : ℕ → α} :
is_cau_seq has_norm.norm u ↔ cauchy_seq u

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

source
@[protected, instance]
def complete_space_of_cau_seq_complete {β : Type v} [normed_field β] [cau_seq.is_complete β has_norm.norm] :
complete_space β

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