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

A Member of a uniformity on \(X\) is a reflexive relation on \(X\).

** lemma ** unif_props:

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

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

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

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

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

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

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

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

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