IsarMathLib

This theory defines uniform spaces and proves their basic properties.

Just like a topological space constitutes the minimal setting in which one can speak of continuous functions, the notion of uniform spaces (commonly attributed to André Weil) captures the minimal setting in which one can speak of uniformly continuous functions. In some sense this is a generalization of the notion of metric (or metrizable) spaces and topological groups.

There are several definitions of uniform spaces. The fact that these definitions are equivalent is far from obvious (some people call such phenomenon cryptomorphism). We will use the definition of the uniform structure (or ''uniformity'') based on entourages. This was the original definition by Weil and it seems to be the most commonly used. A uniformity consists of entourages that are binary relations between points of space \(X\) that satisfy a certain collection of conditions, specified below.

If \(\Phi\) is a uniformity on \(X\), then the every element \(V\) of \(\Phi\) is a certain relation on \(X\) (a subset of \(X\times X\)) and is called an ''entourage''. For an \(x\in X\) we call \(V\{ x\}\) a neighborhood of \(x\). The first useful fact we will show is that neighborhoods are non-empty.

The filter part of the definition of uniformity for easier reference:

The second part of the definition of uniformity for easy reference:

The definition of uniformity states (among other things) that for every member \(U\) of uniformity \(\Phi\) there is another one, say \(V\) such that \(V\circ V\subseteq U\). Sometimes such \(V\) is said to be half the size of \(U\). The next lemma states that \(V\) can be taken to be symmetric.

Inside every member \(W\) of the uniformity \(\Phi\) we can find one that is symmetric and smaller than a third of size \(W\). Compare with the Metamath's theorem with the same name.

If \(\Phi\) is a uniformity on \(X\) then every element of \(\Phi\) is a subset of \(X\times X\) whose domain is \(X\).

If \(\Phi\) is a uniformity on \(X\) and \(W\in \Phi\) the for every \(x\in X\) the image of the singleton \(\{ x\}\) by \(W\) is contained in \(X\). Compare the Metamath's theorem with the same name.

Uniformity \( \Phi \) defines a natural topology on its space \(X\) via the neighborhood system that assigns the collection \(\{V(\{x\}):V\in \Phi\}\) to every point \(x\in X\). In the next lemma we show that if we define a function this way the values of that function are what they should be. This is only a technical fact which is useful to shorten the remaining proofs, usually treated as obvious in standard mathematics.

In the next lemma we show that the collection defined in lemma neigh_filt_fun is a filter on \(X\). The proof is kind of long, but it just checks that all filter conditions hold.

A rephrasing of filter_from_uniformity: if \(\Phi\) is a uniformity on \(X\), then \(\{V(\{ x\}) | V\in \Phi\}\) is a filter on \(X\) for every \(x\in X\).

A frequently used property of filters is that they are "upward closed" i.e. supersets of a filter element are also in the filter. The next lemma makes this explicit for easy reference as applied to the natural filter created from a uniformity.

The function defined in the premises of lemma neigh_filt_fun (or filter_from_uniformity) is a neighborhood system. The proof uses the existence of the "half-the-size" neighborhood condition (\( \exists V\in \Phi .\ V\circ V \subseteq U \)) of the uniformity definition, but not the \( converse(U) \in \Phi \) part.

When we have a uniformity \(\Phi\) on \(X\) we can define a topology on \(X\) in a (relatively) natural way. We will call that topology the \( \text{UniformTopology}(\Phi ) \). We could probably reformulate the definition to skip the \(X\) parameter because if \(\Phi\) is a uniformity on \(X\) then \(X\) can be recovered from (is determined by) \(\Phi\).

An identity showing how the definition of uniform topology is constructed. Here, the \(M = \{\langle t,\{ V\{ t\} : V\in \Phi\}\rangle : t\in X\}\) is the neighborhood system (a function on \(X\)) created from uniformity \(\Phi\). Then for each \(x\in X\), \(M(x) = \{ V\{ t\} : V\in \Phi\}\) is the set of neighborhoods of \(x\).

The collection of sets constructed in the UniformTopology definition is indeed a topology on \(X\).

If we have a uniformity \(\Phi\) we can create a neighborhood system from it in two ways. We can create a a neighborhood system directly from \(\Phi\) using the formula \(X \ni x \mapsto \{V\{x\} | x\in X\}\) (see theorem neigh_from_uniformity). Alternatively we can construct a topology from \(\Phi\) as in theorem uniform_top_is_top and then create a neighborhood system from this topology as in theorem neigh_from_topology. The next theorem states that these two ways give the same result.

Another form of the definition of topology generated from a uniformity.

Images of singletons by entourages are neighborhoods of those singletons.

The set neighborhoods of a singleton \(\{ x\}\) where \(x\in X\) consist of images of the singleton by the entourages \(W\in \Phi\). See also the Metamath's theorem with the same name.

Images of singletons by entourages are set neighborhoods of those singletons. See also the Metamath theorem with the same name.

If \(\Phi\) is a uniformity on \(X\) that generates a topology \(T\), \(R\) is any relation on \(X\) (i.e. \(R\subseteq X\times X\)), \(W\) is a symmetric entourage (i.e. \(W\in \Phi\), and \(W\) is symmetric (i.e. equal to its converse)), then the closure of \(R\) in the product topology is contained the the composition \(V\circ (M \circ V)\). Metamath has a similar theorem with the same name.

Uniform spaces are regular (\(T_3\)).