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 uniform_embedding.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 := (λ 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 uniform_space.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: is_open_iff_ball_subset {s : set X} : is_open 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 id_rel = { 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

• uniform_space X is a uniform space structure on a type X
• uniform_continuous 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 uniform_space X of uniform structures on X, as well as the pullback (uniform_space.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 uniform_space 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:

• [N. Bourbaki, General Topology][bourbaki1966]
• [I. M. James, Topologies and Uniformities][james1999]

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

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

We reformulate the various continuity properties of functions taking values in a uniform space in terms of the uniformity in the target. Since the same lemmas (essentially with the same names) also exist for metric spaces and emetric spaces (reformulating things in terms of the distance or the edistance in the target), we put them in a namespace uniform here.

In the metric and emetric space setting, there are also similar lemmas where one assumes that both the source and the target are metric spaces, reformulating things in terms of the distance on both sides. These lemmas are generally written without primes, and the versions where only the target is a metric space is primed. We follow the same convention here, thus giving lemmas with primes.