Uniform spaces #

Uniform spaces are a generalization of metric spaces and topological groups. Many concepts directly generalize to uniform spaces, e.g.

uniform continuity (in this file)
completeness (in Cauchy.lean)
extension of uniform continuous functions to complete spaces (in IsUniformEmbedding.lean)
totally bounded sets (in Cauchy.lean)
totally bounded complete sets are compact (in Cauchy.lean)

A uniform structure on a type X is a filter 𝓤 X on X × X satisfying some conditions which makes it reasonable to say that ∀ᶠ (p : X × X) in 𝓤 X, ... means "for all p.1 and p.2 in X close enough, ...". Elements of this filter are called entourages of X. The two main examples are:

If X is a metric space, V ∈ 𝓤 X ↔ ∃ ε > 0, { p | dist p.1 p.2 < ε } ⊆ V
If G is an additive topological group, V ∈ 𝓤 G ↔ ∃ U ∈ 𝓝 (0 : G), {p | p.2 - p.1 ∈ U} ⊆ V

Those examples are generalizations in two different directions of the elementary example where X = ℝ and V ∈ 𝓤 ℝ ↔ ∃ ε > 0, { p | |p.2 - p.1| < ε } ⊆ V which features both the topological group structure on ℝ and its metric space structure.

Each uniform structure on X induces a topology on X characterized by

nhds_eq_comap_uniformity : ∀ {x : X}, 𝓝 x = comap (Prod.mk x) (𝓤 X)

where Prod.mk x : X → X × X := (fun y ↦ (x, y)) is the partial evaluation of the product constructor.

The dictionary with metric spaces includes:

an upper bound for dist x y translates into (x, y) ∈ V for some V ∈ 𝓤 X
a ball ball x r roughly corresponds to UniformSpace.ball x V := {y | (x, y) ∈ V} for some V ∈ 𝓤 X, but the later is more general (it includes in particular both open and closed balls for suitable V). In particular we have: isOpen_iff_ball_subset {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 X, ball x V ⊆ s

The triangle inequality is abstracted to a statement involving the composition of relations in X. First note that the triangle inequality in a metric space is equivalent to ∀ (x y z : X) (r r' : ℝ), dist x y ≤ r → dist y z ≤ r' → dist x z ≤ r + r'. Then, for any V and W with type Set (X × X), the composition V ○ W : Set (X × X) is defined as { p : X × X | ∃ z, (p.1, z) ∈ V ∧ (z, p.2) ∈ W }. In the metric space case, if V = { p | dist p.1 p.2 ≤ r } and W = { p | dist p.1 p.2 ≤ r' } then the triangle inequality, as reformulated above, says V ○ W is contained in {p | dist p.1 p.2 ≤ r + r'} which is the entourage associated to the radius r + r'. In general we have mem_ball_comp (h : y ∈ ball x V) (h' : z ∈ ball y W) : z ∈ ball x (V ○ W). Note that this discussion does not depend on any axiom imposed on the uniformity filter, it is simply captured by the definition of composition.

The uniform space axioms ask the filter 𝓤 X to satisfy the following:

every V ∈ 𝓤 X contains the diagonal idRel = { p | p.1 = p.2 }. This abstracts the fact that dist x x ≤ r for every non-negative radius r in the metric space case and also that x - x belongs to every neighborhood of zero in the topological group case.
V ∈ 𝓤 X → Prod.swap '' V ∈ 𝓤 X. This is tightly related the fact that dist x y = dist y x in a metric space, and to continuity of negation in the topological group case.
∀ V ∈ 𝓤 X, ∃ W ∈ 𝓤 X, W ○ W ⊆ V. In the metric space case, it corresponds to cutting the radius of a ball in half and applying the triangle inequality. In the topological group case, it comes from continuity of addition at (0, 0).

These three axioms are stated more abstractly in the definition below, in terms of operations on filters, without directly manipulating entourages.

Main definitions #

UniformSpace X is a uniform space structure on a type X
UniformContinuous f is a predicate saying a function f : α → β between uniform spaces is uniformly continuous : ∀ r ∈ 𝓤 β, ∀ᶠ (x : α × α) in 𝓤 α, (f x.1, f x.2) ∈ r

In this file we also define a complete lattice structure on the type UniformSpace X of uniform structures on X, as well as the pullback (UniformSpace.comap) of uniform structures coming from the pullback of filters. Like distance functions, uniform structures cannot be pushed forward in general.

Notations #

Localized in Uniformity, we have the notation 𝓤 X for the uniformity on a uniform space X, and ○ for composition of relations, seen as terms with type Set (X × X).

Implementation notes #

There is already a theory of relations in Data/Rel.lean where the main definition is def Rel (α β : Type*) := α → β → Prop. The relations used in the current file involve only one type, but this is not the reason why we don't reuse Data/Rel.lean. We use Set (α × α) instead of Rel α α because we really need sets to use the filter library, and elements of filters on α × α have type Set (α × α).

The structure UniformSpace X bundles a uniform structure on X, a topology on X and an assumption saying those are compatible. This may not seem mathematically reasonable at first, but is in fact an instance of the forgetful inheritance pattern. See Note [forgetful inheritance] below.

References #

The formalization uses the books:

But it makes a more systematic use of the filter library.

Uniform spaces #

Main definitions #

Notations #

Implementation notes #

References #

Relations, seen as Set (α × α) #

Balls in uniform spaces #

Neighborhoods in uniform spaces #

Closure and interior in uniform spaces #

Uniformity bases #

Uniform continuity #

Expressing continuity properties in uniform spaces #

Relations, seen as `Set (α × α)` #