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:

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\)).

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 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.