Cauchy

Space of Cauchy filters

This is essentially the completion of a uniform space. The embeddings are the neighbourhood filters. This space is not minimal, the separated uniform space (i.e. quotiented on the intersection of all entourages) is necessary for this.

Cauchy.pure_cauchy

Embedding of α into its completion

uniform_space.completion

Hausdorff completion of α

uniform_space.completion.has_coe_t

Automatic coercion from α to its completion. Not always injective.

uniform_space.completion.extension

"Extension" to the completion. It is defined for any map f but returns an arbitrary constant value if f is not uniformly continuous

uniform_space.completion.map

Completion functor acting on morphisms