An auxiliary positive sequence that tends to 0 in ennreal, with good behavior.

Auxiliary sequence, which is bounded by B, positive, and tends to 0.

Define a decreasing sequence of sets in the filter f, of diameter bounded by B2 n.

These sets are in the filter.

These sets are nonempty.

By construction, their diameter is controlled by B2 n.

These sets are nested.

Define the approximating Cauchy sequence for the Cauchy filter f, obtained by taking a point in each set.

The approximating sequence indeed belong to our good sets.

The distance between points in the sequence is bounded by B2 N.

The approximating sequence is indeed Cauchy as B2 n tends to 0 with n.

If the approximating Cauchy sequence is converging, to a limit y, then the original Cauchy filter f is also converging, to the same limit. Given t1 in the filter f and t2 a neighborhood of y, it suffices to show that t1 ∩ t2 is nonempty. Pick ε so that the ε-eball around y is contained in t2. Pick n with B2 n < ε/2, and n2 such that dist(seq n2, y) < ε/2. Let N = max(n, n2). We defined seq by looking at a decreasing sequence of sets of f with shrinking radius. The Nth one has radius < B2 N < ε/2. This set is in f, so we can find an element x that's also in t1. dist(x, seq N) < ε/2 since seq N is in this set, and dist (seq N, y) < ε/2, so x is in the ε-ball around y, and thus in t2.

An emetric space in which every Cauchy sequence converges is complete.

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form edist (u n) (u m) < B N for all n m ≥ N are converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to 0, which makes it possible to use arguments of converging series, while this is impossible to do in general for arbitrary Cauchy sequences.

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form dist (u n) (u m) < B N for all n m ≥ N are converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to 0, which makes it possible to use arguments of converging series, while this is impossible to do in general for arbitrary Cauchy sequences.

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

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