A filter f is Cauchy if for every entourage r, there exists an s ∈ f such that s × s ⊆ r. This is a generalization of Cauchy sequences, because if a : ℕ → α then the filter of sets containing cofinitely many of the a n is Cauchy iff a is a Cauchy sequence.

Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that is general enough to cover both ℕ and ℝ, which are the main motivating examples.

A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.

If univ is complete, the space is a complete space

A Cauchy sequence in a complete space converges

If K is a complete subset, then any cauchy sequence in K converges to a point in K

A set s is totally bounded if for every entourage d there is a finite set of points t such that every element of s is d-near to some element of t.