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
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)
@[instance]
Equations
In a normed field, cau_seq coincides with the usual notion of Cauchy sequences.
@[instance]
def
complete_space_of_cau_seq_complete
{β : Type v}
[normed_field β]
[cau_seq.is_complete β has_norm.norm] :
A complete normed field is complete as a metric space, as Cauchy sequences converge by assumption and this suffices to characterize completeness.