Theorems · Inductive type · general topology

UniformSpace

Type u → Type u

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.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

2,040 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms