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 \), \( W\in \Phi \)** and **\( x\in X \)

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

** lemma ** unif_filter:

** assumes **\( \Phi \text{ is a uniformity on } X \)

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

** lemma ** entourage_props:

** assumes **\( \Phi \text{ is a uniformity on } X \)** and **\( A\in \Phi \)

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.

** lemma ** half_size_symm:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)

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.

** lemma ** ustex3sym:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( A\in \Phi \)

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

** lemma ** uni_domain:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)

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.

** lemma ** ustimasn:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)** and **\( x\in X \)

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.

** 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\} \)

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.

** 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\} \)

{
** fix **\( B \) ** assume **\( B \in \mathcal{M} (x) \)
** fix **\( C \) ** assume **\( C \in Pow(X) \)** and **\( B\subseteq C \)
** from **\( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \), \( B \in \mathcal{M} (x) \) ** obtain **\( U \)** where **\( U\in \Phi \)** and **\( B = U\{x\} \)
** let **\( V = U \cup C\times C \) ** from **assms, \( U\in \Phi \), \( C \in Pow(X) \) ** have ** \( V \in Pow(X\times X) \)** and **\( U\subseteq V \)** using ** IsUniformity_def, IsFilter_def
** with **\( U\in \Phi \), PhiFilter ** have ** \( V\in \Phi \)** using ** IsFilter_def
** moreover ** ** from **assms, \( U\in \Phi \), \( x\in X \), \( B = U\{x\} \), \( B\subseteq C \) ** have ** \( C = V\{x\} \)** using ** neigh_not_empty, image_greater_rel
** ultimately **** have ** \( C \in \{V\{x\}.\ V\in \Phi \} \)
** with **\( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) ** have ** \( C \in \mathcal{M} (x) \)
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( A \) \( B \) ** assume **\( A \in \mathcal{M} (x) \)** and **\( B \in \mathcal{M} (x) \)
** with **\( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) ** obtain **\( V_A \) \( V_B \)** where **\( A = V_A\{x\} \), \( B = V_B\{x\} \)** and **\( V_A \in \Phi \), \( V_B \in \Phi \)
** let **\( C = V_A\{x\} \cap V_B\{x\} \) ** from **assms, \( V_A \in \Phi \), \( V_B \in \Phi \) ** have ** \( V_A\cap V_B \in \Phi \)** using ** IsUniformity_def, IsFilter_def
** with **\( \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \} \) ** have ** \( (V_A\cap V_B)\{x\} \in \mathcal{M} (x) \)
** moreover ** ** from **PhiFilter, \( V_A \in \Phi \), \( V_B \in \Phi \) ** have ** \( C \in Pow(X) \)** unfolding ** IsFilter_def
** moreover ** ** have ** \( (V_A\cap V_B)\{x\} \subseteq C \)** using ** image_Int_subset_left
** moreover ** ** note **LargerIn
** ultimately **** have ** \( C \in \mathcal{M} (x) \)
** with **\( A = V_A\{x\} \), \( B = V_B\{x\} \) ** have ** \( A\cap B \in \mathcal{M} (x) \)
** } **
** thus ** \( thesis \)
** qed **

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

** lemma ** unif_filter_at_point:

** assumes **\( \Phi \text{ is a uniformity on } X \)** and **\( 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.

** corollary ** unif_filter_up_closed:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( x\in X \), \( U \in \{V\{x\}.\ V\in \Phi \} \), \( W\subseteq X \), \( U\subseteq W \)

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.

** theorem ** neigh_from_uniformity:

** assumes **\( \Phi \text{ is a uniformity on } X \)

{
** fix **\( N \) ** assume **\( N\in \mathcal{M} (x) \)
** have ** \( x\in N \)** and **\( \exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N \in \mathcal{M} (y)) \)proof
** from **\( \mathcal{M} :X\rightarrow Pow(Pow(X)) \), Mval, \( x\in X \), \( N\in \mathcal{M} (x) \) ** obtain **\( U \)** where **\( U\in \Phi \)** and **\( N = U\{x\} \)
** with **assms, \( x\in X \) ** show ** \( x\in N \)** using ** neigh_not_empty
** from **assms, \( U\in \Phi \) ** obtain **\( V \)** where **\( V\in \Phi \)** and **\( V\circ V \subseteq U \)** unfolding ** IsUniformity_def
** let **\( W = V\{x\} \)
** from **\( V\in \Phi \), Mval, \( x\in X \) ** have ** \( W \in \mathcal{M} (x) \)
** moreover ** ** have ** \( \forall y\in W.\ N \in \mathcal{M} (y) \)proof
** ultimately **** show ** \( \exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N \in \mathcal{M} (y)) \)
** qed **
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( y \) ** assume **\( y\in W \)
** with **\( \mathcal{M} :X\rightarrow Pow(Pow(X)) \), \( x\in X \), \( W \in \mathcal{M} (x) \) ** have ** \( y\in X \)** using ** apply_funtype
** with **assms ** have ** \( \mathcal{M} (y) \text{ is a filter on } X \)** using ** filter_from_uniformity
** moreover ** ** from **assms, \( y\in X \), \( V\in \Phi \) ** have ** \( V\{y\} \in \mathcal{M} (y) \)** using ** neigh_filt_fun
** moreover ** ** from **\( \mathcal{M} :X\rightarrow Pow(Pow(X)) \), \( x\in X \), \( N \in \mathcal{M} (x) \) ** have ** \( N \in Pow(X) \)** using ** apply_funtype
** moreover ** ** from **\( V\circ V \subseteq U \), \( y\in W \) ** have ** \( V\{y\} \subseteq (V\circ V)\{x\} \)** and **\( (V\circ V)\{x\} \subseteq U\{x\} \)
** with **\( N = U\{x\} \) ** have ** \( V\{y\} \subseteq N \) ** ultimately **** have ** \( N \in \mathcal{M} (y) \)** unfolding ** IsFilter_def
** } **
** thus ** \( thesis \)
** qed **

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

** definition **

\( \text{UniformTopology}(\Phi ,X) \equiv \{U\in Pow(X).\ \forall x\in U.\ U\in \{V\{x\}.\ V\in \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\).

** lemma ** uniftop_def_alt:

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

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.

** theorem ** neigh_unif_same:

** assumes **\( \Phi \text{ is a uniformity on } X \)

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

** lemma ** uniftop_def_alt1:

** assumes **\( \Phi \text{ is a uniformity on } X \)

Images of singletons by entourages are neighborhoods of those singletons.

** lemma ** image_singleton_ent_nei:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( V\in \Phi \), \( x\in X \)

** defines **\( \mathcal{M} \equiv \text{ neighborhood system of } \text{UniformTopology}(\Phi ,X) \)

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.

** lemma ** utopsnneip:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( x\in X \)

** defines **\( \mathcal{S} \equiv \text{ set neighborhood system of } \text{UniformTopology}(\Phi ,X) \)

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

** corollary ** utopsnnei:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \), \( x\in X \)

** defines **\( \mathcal{S} \equiv \text{ set neighborhood system of } \text{UniformTopology}(\Phi ,X) \)

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.

** lemma ** utop3cls:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( R\subseteq X\times X \), \( W\in \Phi \), \( W=converse(W) \)

** defines **\( J \equiv \text{UniformTopology}(\Phi ,X) \)

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

** theorem ** utopreg:

** assumes **\( \Phi \text{ is a uniformity on } X \)

{
** fix **\( U \) \( x \) ** assume **\( U\in J \), \( x\in U \)
** then **** have ** \( U \in \mathcal{S} \{x\} \)** using ** open_nei_singl
** from **\( U\in J \) ** have ** \( U\subseteq \bigcup J \)
** with **\( x\in U \), \( \bigcup J = X \) ** have ** \( x\in X \)
** from **assms(1), \( x\in X \), \( U \in \mathcal{S} \{x\} \) ** obtain **\( A \)** where **\( U=A\{x\} \)** and **\( A\in \Phi \)** using ** utopsnneip
** from **assms(1), \( A\in \Phi \) ** obtain **\( W \)** where **\( W\in \Phi \), \( W\circ (W\circ W) \subseteq A \)** and **Wsymm: \( W=converse(W) \)** using ** ustex3sym
** with **assms(1), \( x\in X \) ** have ** \( W\{x\} \in \mathcal{S} \{x\} \)** and **\( W\{x\} \subseteq X \)** using ** utopsnnei, ustimasn
** from **\( W\{x\} \in \mathcal{S} \{x\} \) ** have ** \( \exists V\in J.\ \{x\}\subseteq V \wedge V\subseteq W\{x\} \)** by (rule **neii2** ) **
** then **** obtain **\( V \)** where **\( V\in J \), \( x\in V \), \( V\subseteq W\{x\} \)
** have ** \( \text{Closure}(V,J) \subseteq U \)proof
** from **assms(1), \( W\in \Phi \), \( \bigcup J = X \) ** have ** \( W \subseteq X\times X \)** using ** entourage_props(1)
** from **cntx, \( W\{x\} \subseteq X \), \( \bigcup J = X \), \( V\subseteq W\{x\} \) ** have ** \( \text{Closure}(V,J) \subseteq \text{Closure}(W\{x\},J) \)** using ** top_closure_mono
** also ** ** have ** \( \text{Closure}(W\{x\},J) \subseteq \text{Closure}(W,J\times _tJ)\{x\} \)proof
** from **\( W\subseteq X\times X \), \( x\in X \), \( \bigcup J = X \) ** have ** \( W\subseteq (\bigcup J)\times (\bigcup J) \), \( x\in \bigcup J \)
** with **\( J \text{ is a topology } \) ** show ** \( thesis \)** using ** imasncls
** qed **
** also ** ** from **assms(1), \( W\subseteq X\times X \), \( W\in \Phi \), Wsymm, \( W\circ (W\circ W) \subseteq A \) ** have ** \( \text{Closure}(W,J\times _tJ)\{x\} \subseteq A\{x\} \)** using ** utop3cls
** finally **** have ** \( \text{Closure}(V,J) \subseteq A\{x\} \)
** with **\( U=A\{x\} \) ** show ** \( thesis \)
** qed **
** with **\( V\in J \), \( x\in V \) ** have ** \( \exists V\in J.\ x\in V \wedge \text{Closure}(V,J)\subseteq U \)
** } **
** thus ** \( thesis \)
** qed **

Definition of IsUniformity:
\( \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 ) \)

Definition of IsFilter:
\( \mathfrak{F} \text{ is a filter on } X \equiv (0\notin \mathfrak{F} ) \wedge (X\in \mathfrak{F} ) \wedge \mathfrak{F} \subseteq Pow(X) \wedge \)
\( (\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} ) \wedge (\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} ) \)

** assumes **\( \Phi \text{ is a uniformity on } X \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)

** assumes **\( \Phi \text{ is a uniformity on } X \)** and **\( A\in \Phi \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)

** assumes **\( \forall x\in X.\ b(x) \in Y \)

** assumes **\( f:X\rightarrow Y \), \( x\in X \)** and **\( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

** assumes **\( \Phi \text{ is a uniformity on } X \)

** defines **\( \mathcal{M} \equiv \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)** and **\( x\in X \)

** assumes **\( x \in U\{x\} \)** and **\( U\{x\} \subseteq 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\} \)

** assumes **\( x\in X \)

Definition of IsNeighSystem:
\( \mathcal{M} \text{ is a neighborhood system on } X \equiv (\mathcal{M} : X\rightarrow Pow(Pow(X))) \wedge \)
\( (\forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X) \wedge (\forall N\in \mathcal{M} (x).\ x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y)) ) )) \)

Definition of UniformTopology:
\( \text{UniformTopology}(\Phi ,X) \equiv \{U\in Pow(X).\ \forall x\in U.\ U\in \{V\{x\}.\ V\in \Phi \}\} \)

** assumes **\( \Phi \text{ is a uniformity 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)\} \)

** 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)\} \)

** assumes **\( \Phi \text{ is a uniformity on } X \)** and **\( x\in X \)

** assumes **\( \mathfrak{F} \text{ is a filter on } X \)

** assumes **\( \Phi \text{ is a uniformity on } X \)

** assumes **\( \Phi \text{ is a uniformity on } X \)

** assumes **\( x\in \bigcup T \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( x\in X \)

** defines **\( \mathcal{S} \equiv \text{ set neighborhood system of } \text{UniformTopology}(\Phi ,X) \)

** assumes **\( \Phi \text{ is a uniformity on } X \)

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \)

** assumes **\( A \subseteq \bigcup T \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \), \( x\in X \)

** defines **\( \mathcal{S} \equiv \text{ set neighborhood system of } \text{UniformTopology}(\Phi ,X) \)

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \)** and **\( A \in (\text{ set neighborhood system of } T)(C) \)** and **\( B \in (\text{ set neighborhood system of } S)(D) \)

** assumes **\( T \text{ is a topology } \), \( A\subseteq \bigcup T \), \( x \in \text{Closure}(A,T) \)** and **\( N \in (\text{ set neighborhood system of } T)\{x\} \)

** assumes **\( W=converse(W) \)** and **\( (W\{x\})\times (W\{y\}) \cap R \neq 0 \)

** assumes **\( V\in T \), \( x\in V \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( A\in \Phi \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( W\in \Phi \)** and **\( x\in X \)

** assumes **\( N \in (\text{ set neighborhood system of } T)(A) \)

** assumes **\( \Phi \text{ is a uniformity on } X \)** and **\( A\in \Phi \)

** assumes **\( B \subseteq \bigcup T \)** and **\( A\subseteq B \)

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \), \( R \subseteq (\bigcup T)\times (\bigcup S) \), \( x\in \bigcup T \)

** assumes **\( \Phi \text{ is a uniformity on } X \), \( R\subseteq X\times X \), \( W\in \Phi \), \( W=converse(W) \)

** defines **\( J \equiv \text{UniformTopology}(\Phi ,X) \)

** assumes **\( T \text{ is a topology } \)