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.
Definition
\( \Phi \text{ is a uniformity on } X \equiv (\Phi \text{ is a filter on } (X\times X))\) \( \wedge (\forall U\in \Phi .\ id(X) \subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi ) \)
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.
lemma neigh_not_empty:
assumes \( \Phi \text{ is a uniformity on } X \), \( V\in \Phi \) and \( x\in X \)
shows \( V\{x\} \neq 0 \) and \( x \in V\{x\} \)proofUniformity \( \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.
lemma neigh_filt_fun:
assumes \( \Phi \text{ is a uniformity on } X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \) and \( \forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \)proofIn 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.
lemma filter_from_uniformity:
assumes \( \Phi \text{ is a uniformity on } X \) and \( x\in X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} (x) \text{ is a filter on } X \)proofThe 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.
theorem neigh_from_uniformity:
assumes \( \Phi \text{ is a uniformity on } X \)
shows \( \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \text{ is a neighborhood system on } X \)proofWhen 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 ) \). The definition may be a bit cryptic but it just combines the construction of a neighborhood system from uniformity as in the assumptions of lemma filter_from_uniformity and the construction of topology from a neighborhood system from theorem topology_from_neighs. 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\).
Definition
\( \text{UniformTopology}(\Phi ,X) \equiv \{U \in Pow(X).\ \forall x\in U.\ U \in \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\}(x)\} \)
The collection of sets constructed in the UniformTopology definition is indeed a topology on \(X\).
theorem uniform_top_is_top:
assumes \( \Phi \text{ is a uniformity on } X \)
shows \( \text{UniformTopology}(\Phi ,X) \text{ is a topology } \) and \( \bigcup \text{UniformTopology}(\Phi ,X) = X \) using assms , neigh_from_uniformity , UniformTopology_def , topology_from_neighsassumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \)assumes \( \Phi \text{ is a uniformity on } X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} :X\rightarrow Pow(Pow(X)) \) and \( \forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \)assumes \( \Phi \text{ is a uniformity on } X \), \( V\in \Phi \) and \( x\in X \)
shows \( V\{x\} \neq 0 \) and \( x \in V\{x\} \)assumes \( x \in U\{x\} \) and \( U\{x\} \subseteq C \)
shows \( (U \cup C\times C)\{x\} = C \)assumes \( \Phi \text{ is a uniformity on } X \) and \( x\in X \)
defines \( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)
shows \( \mathcal{M} (x) \text{ is a filter on } X \)assumes \( \Phi \text{ is a uniformity on } X \)
shows \( \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \text{ is a neighborhood system on } X \)assumes \( \mathcal{M} \text{ is a neighborhood system on } X \)
defines \( T \equiv \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} \)
shows \( T \text{ is a topology } \) and \( \bigcup T = X \)