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.

Since the whole \(X\times X\) is in a uniformity, a uniformity is never empty.

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:

If \(X\) is not empty then the singleton \(\{ X\times X\}\) is a (trivial) example of a uniformity on \(X\).

On the other side of the spectrum is the collection of sets containing the diagonal, that is also a uniformity.

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\} | V\in \Phi\}\) (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. Note that is not the same as \(T_3\), see Topology_ZF_1 for separation axioms definitions. In some sources the definitions of "regular" and \(T_3\) are swapped. In IsarMathLib we adopt the terminology as on the "Separation axiom" page on Wikipedia.

If the topological space generated by a uniformity \(\Phi\) on \(X\) is \(T_1\) then the intersection \(\bigcup \Phi\) is contained in the diagonal \(\{\langle x,x\rangle : x\in X\}\). Note the opposite inclusion is true for every uniformity.

If the intersection of a uniformity is contained in the the diagonal \(\{\langle x,x\rangle : x\in X\}\) then the topological space generated by this uniformity is \(T_1\).

If \(\Phi\) is a uniformity on \(X\) then the intersection of \(\Phi\) is contained in diagonal of \(X\) if and only if \(\bigcup \Phi\) is equal to that diagonal. Some people call such uniform space "separating".

The next theorem collects the information we have to show that if \(\Phi\) is a uniformity on \(X\), with the induced topology \(T\) then conditions \(T\) is \(T_0\), \(T\) is \(T_1\), \(T\) is \(T_2\) \(T\) is \(T_3\) are all equivalent to the intersection of \(\Phi\) being contained in the diagonal (which is equivalent to the intersection of \(\Phi\) being equal to the diagonal, see unif_inter_diag above.

A base or a fundamental system of entourages of a uniformity \(\Phi\) is a subset of \(\Phi\) that is sufficient to uniquely determine it. This is analogous to the notion of a base of a topology (see Topology_ZF_1 or a base of a filter (see Topology_ZF_4).

A base of a uniformity \(\Phi\) is any subset \(\mathfrak{B}\subseteq \Phi\) such that every entourage in \(\Phi\) contains (at least) one from \(\mathfrak{B}\). The phrase is a base for is already defined to mean a base for a topology, so we use the phrase is a uniform base of here.

Symmetric entourages form a base of the uniformity.

Given a base of a uniformity we can recover the uniformity taking the supersets. The Supersets constructor is defined in ZF1.

Analogous to the predicate "satisfies base condition" (defined in Topology_ZF_1) and "is a base filter" (defined in Topology_ZF_4) we can specify conditions for a collection \(\mathfrak{B}\) of subsets of \(X\times X\) to be a base of some uniformity on \(X\). Namely, the following conditions are necessary and sufficient:

1. Intersection of two sets of \(\mathfrak{B}\) contains a set of \(\mathfrak{B}\).

2. Every set of \(\mathfrak{B}\) contains the diagonal of \(X\times X\).

3. For each set \(B_1\in \mathfrak{B}\) we can find a set \(B_2\in \mathfrak{B}\) such that \(B_2\subseteq B_1^{-1}\).

4. For each set \(B_1\in \mathfrak{B}\) we can find a set \(B_2\in \mathfrak{B}\) such that \(B_2\circ B_2 \subseteq B_1\).

The conditions in the definition below are taken from N. Bourbaki "Elements of Mathematics, General Topology", Chapter II.1., except for the last two that are missing there.

The next lemma splits the definition of IsUniformityBaseOn into four conditions to enable more precise references in proofs.

If supersets of some collection of subsets of \(X\times X\) form a uniformity, then this collection satisfies the conditions in the definition of IsUniformityBaseOn.

if a nonempty collection of subsets of \(X\times X\) satisfies conditions in the definition of IsUniformityBaseOn then the supersets of that collection form a uniformity on \(X\).

The assumption that \(X\) is not empty in uniformity_base_is_base above is neccessary as the assertion is false if \(X\) is empty.

Uniformities on a set \(X\) are naturally ordered by the inclusion relation. Specifically, for two uniformities \(\mathcal{U}_1\) and \(\mathcal{U}_2\)​ on a set \(X\) if \(\mathcal{U}_1 \subseteq \mathcal{U}_2\) we say that \(\mathcal{U}_2\) is finer than \(\mathcal{U}_1\) or that \(\mathcal{U}_1\) is coarser than \(\mathcal{U}_2\). Turns out this order is complete: every nonempty set of uniformities has a least upper bound, i.e. a supremum.

We define \( \text{Uniformities}(X) \) as the set of all uniformities on \(X\).

If \(\Phi\) is a uniformity on \(X\), then \(\Phi\) is a collection of subsets of \(X\times X\), hence it's a member of \( \text{Uniformities}(X) \).

For nonempty sets the set of uniformities is not empty as well.

Uniformities on a set \(X\) are naturally ordered by inclusion, we call the resulting order relation OrderOnUniformities.

The order defined by inclusion on uniformities is a partial order.

In particular, the order defined by inclusion on uniformities is antisymmetric. Having this as a separate fact is handy as we reference some lemmas proven for antisymmetric (not necessarily partial order) relations.

If \(X\) is not empty then the singleton \(\{ X\times X\}\) is the minimal element of the set of uniformities on \(X\) ordered by inclusion and the collection of subsets of \(X\times X\) that contain the diagonal is the maximal element.

Given a set of uniformities \(\mathcal{U}\) on \(X\) we define a collection of subsets of \(X\) called LUB_UnifBase (the least upper bound base in comments) as the set of all products of nonempty finite subsets of \(\bigcup\mathcal{U}\). The "least upper bound base" term is not justified at this point, but we will show later that this set is actually a uniform base (i.e. a fundamental system of entourages) on \(X\) and hence the supersets of it form a uniformity on \(X\), which is the supremum (i.e. the least upper bound) of \(\mathcal{U}\).

For any two sets in the least upper bound base there is a third one contained in both.

Each set in the least upper bound base contains the diagonal of \(X\times X\).

The converse of each set from the least upper bound base contains a set from it.

For each set (relation) \(U_1\) from the least upper bound base there is another one \(U_2\) such that \(U_2\) composed with itself is contained in \(U_1\).

The least upper bound base is a collection of relations on \(X\).

If a collection of uniformities is nonempty, then the least upper bound base is non-empty as well.

If a collection of uniformities \(\mathcal{U}\) is nonempty, \(\mathcal{B}\) denotes the least upper bound base for \(\mathcal{U}\), then \(\mathcal{B}\) is a uniform base on \(X\), hence its supersets form a uniformity on \(X\) and the uniform topology generated by that uniformity is indeed a topology on \(X\).

At this point we know that supersets with respect to \(X\times X\) of the least upper bound base for a collection of uniformities \(\mathcal{U}\) form a uniformity. To shorten the notation we will call this uniformity \( \text{LUB_Unif}(X,\mathcal{U} ) \).

For any collection of uniformities \(\mathcal{U}\) on a nonempty set \(X\) the \( \text{LUB_Unif}(X,\mathcal{U} ) \) collection defined above is indeed an upper bound of \(\mathcal{U}\) in the order defined by the inclusion relation.

Any upper bound (in the order defined by inclusion relation) of a nonempty collection of uniformities \(\mathcal{U}\) on a nonempty set \(X\) is greater or equal (in that order) than \( \text{LUB_Unif}(X,\mathcal{U} ) \). Together with lub_unif_upper_bound it means that \( \text{LUB_Unif}(X,\mathcal{U} ) \) is indeed the least upper bound of \(\mathcal{U}\).

A nonempty collection \(\mathcal{U}\) of uniformities on \(X\) has a supremum (i.e. the least upper bound).

The order on uniformities derived from inclusion is complete.