The identity relation, or the graph of the identity function

The composition of relations

This core description of a uniform space is outside of the type class hierarchy. It is useful for constructions of uniform spaces, when the topology is derived from the uniform space.

A uniform space generates a topological space

A uniform space is a generalization of the "uniform" topological aspects of a metric space. It consists of a filter on α × α called the "uniformity", which satisfies properties analogous to the reflexivity, symmetry, and triangle properties of a metric.

A metric space has a natural uniformity, and a uniform space has a natural topology. A topological group also has a natural uniformity, even when it is not metrizable.

The uniformity is a filter on α × α (inferred from an ambient uniform space structure on α).

Given f : α → β and a uniformity u on β, the inverse image of u under f is the inverse image in the filter sense of the induced function α × α → β × β.

Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained by taking independently an entourage of the diagonal in the first part, and an entourage of the diagonal in the second part.

The union of an entourage of the diagonal in each set of a disjoint union is again an entourage of the diagonal.