Theorems · Definition · general topology

CauchyFilter

(α : Type u) → [UniformSpace α] → Type u

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.

Defined in

Mathlib.Topology.UniformSpace.Completion

Cited by

19 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpace