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

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

** lemma ** uniformity_non_empty:

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

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

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.

** definition **

\( \mathfrak{B} \text{ is a uniform base of } \Phi \equiv \mathfrak{B} \subseteq \Phi \wedge (\forall U\in \Phi .\ \exists B\in \mathfrak{B} .\ B\subseteq U) \)

Symmetric entourages form a base of the uniformity.

** lemma ** symm_are_base:

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

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

** lemma ** uniformity_from_base:

** assumes **\( \Phi \text{ is a uniformity on } X \), \( \mathfrak{B} \text{ is a uniform base of } \Phi \)

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.

** definition **

\( \mathfrak{B} \text{ is a uniform base on } X \equiv \) \( (\forall B_1\in \mathfrak{B} .\ \forall B_2\in \mathfrak{B} .\ \exists B_3\in \mathfrak{B} .\ B_3\subseteq B_1\cap B_2) \wedge (\forall B\in \mathfrak{B} .\ id(X)\subseteq B) \wedge \) \( (\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)) \wedge (\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1) \wedge \) \( \mathfrak{B} \subseteq Pow(X\times X) \wedge \mathfrak{B} \neq \emptyset \)

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

** lemma ** uniformity_base_props:

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)

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

** theorem ** base_is_uniform_base:

** assumes **\( \mathfrak{B} \subseteq Pow(X\times X) \)** and **\( \text{Supersets}(X\times X,\mathfrak{B} ) \text{ is a uniformity on } X \)

{
** fix **\( B_1 \) \( B_2 \) ** assume **\( B_1\in \mathfrak{B} \), \( B_2\in \mathfrak{B} \)
** with **assms(1) ** have ** \( B_1\in \Phi \)** and **\( B_2\in \Phi \)** unfolding ** Supersets_def
** with **assms(2) ** have ** \( \exists B_3\in \mathfrak{B} .\ B_3 \subseteq B_1\cap B_2 \)** unfolding ** IsUniformity_def, IsFilter_def, Supersets_def
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( B \) ** assume **\( B\in \mathfrak{B} \)
** with **assms(1) ** have ** \( B\in \Phi \)** unfolding ** Supersets_def
** with **assms(2) ** have ** \( id(X)\subseteq B \)** unfolding ** IsUniformity_def
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( B_1 \) ** assume **\( B_1\in \mathfrak{B} \)
** with **assms(1) ** have ** \( B_1\in \Phi \)** unfolding ** Supersets_def
** with **assms ** have ** \( \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1) \)** unfolding ** IsUniformity_def, Supersets_def
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( B_1 \) ** assume **\( B_1\in \mathfrak{B} \)
** with **assms(1) ** have ** \( B_1\in \Phi \)** unfolding ** Supersets_def
** with **assms(2) ** obtain **\( V \)** where **\( V\in \Phi \)** and **\( V\circ V \subseteq B_1 \)** unfolding ** IsUniformity_def
** from **assms(2), \( V\in \Phi \) ** obtain **\( B_2 \)** where **\( B_2\in \mathfrak{B} \)** and **\( B_2\subseteq V \)** unfolding ** Supersets_def
** from **\( V\circ V \subseteq B_1 \), \( B_2\subseteq V \) ** have ** \( B_2\circ B_2 \subseteq B_1 \)
** with **\( B_2\in \mathfrak{B} \) ** have ** \( \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1 \)
** } **
** thus ** \( thesis \)
** qed **

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

** theorem ** uniformity_base_is_base:

** assumes **\( X\neq \emptyset \)** and **\( \mathfrak{B} \text{ is a uniform base on } X \)

{
** fix **\( U \) \( V \) ** assume **\( U\in \Phi \), \( V\in \Phi \)
** then **** obtain **\( B_1 \) \( B_2 \)** where **\( B_1\in \mathfrak{B} \), \( B_2\in \mathfrak{B} \), \( B_1\subseteq U \), \( B_2\subseteq V \)** unfolding ** Supersets_def
** from **assms(2), \( B_1\in \mathfrak{B} \), \( B_2\in \mathfrak{B} \) ** obtain **\( B_3 \)** where **\( B_3\in \mathfrak{B} \)** and **\( B_3\subseteq B_1\cap B_2 \)** using ** uniformity_base_props(1)
** from **\( B_1\subseteq U \), \( B_2\subseteq V \), \( B_3\subseteq B_1\cap B_2 \) ** have ** \( B_3\subseteq U\cap V \)
** with **\( U\in \Phi \), \( V\in \Phi \), \( B_3\in \mathfrak{B} \) ** have ** \( U\cap V \in \Phi \)** unfolding ** Supersets_def
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( U \) \( C \) ** assume **\( U\in \Phi \), \( C\in Pow(X\times X) \), \( U\subseteq C \)
** from **\( U\in \Phi \) ** obtain **\( B \)** where **\( B\in \mathfrak{B} \)** and **\( B\subseteq U \)** unfolding ** Supersets_def
** with **\( U\subseteq C \), \( C\in Pow(X\times X) \) ** have ** \( C\in \Phi \)** unfolding ** Supersets_def
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( U \) ** assume **\( U\in \Phi \)
** then **** obtain **\( B \)** where **\( B\in \mathfrak{B} \)** and **\( B\subseteq U \)** unfolding ** Supersets_def
** with **assms(2) ** have ** \( id(X) \subseteq U \)** using ** uniformity_base_props(2)
** moreover ** ** from **assms(2), \( B\in \mathfrak{B} \) ** obtain **\( V \)** where **\( V\in \mathfrak{B} \)** and **\( V\circ V \subseteq B \)** using ** uniformity_base_props(4)
** with **\( \mathfrak{B} \subseteq Pow(X\times X) \) ** have ** \( V\in \Phi \)** using ** superset_gen
** with **\( V\circ V \subseteq B \), \( B\subseteq U \) ** have ** \( \exists V\in \Phi .\ V\circ V \subseteq U \) ** moreover ** ** from **assms(2), \( B\in \mathfrak{B} \), \( B\subseteq U \) ** obtain **\( W \)** where **\( W\in \mathfrak{B} \)** and **\( W \subseteq converse(U) \)** using ** uniformity_base_props(3)
** with **\( U\in \Phi \) ** have ** \( converse(U) \in \Phi \)** unfolding ** Supersets_def ** ultimately **** have ** \( id(X) \subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi \)
** } **
** thus ** \( thesis \)
** qed **

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

** lemma ** uniform_space_empty:

** assumes **\( \mathfrak{B} \text{ is a uniform base on } \emptyset \)

{
** let **\( \Phi = \text{Supersets}(\emptyset \times \emptyset ,\mathfrak{B} ) \) ** assume **\( \Phi \text{ is a uniformity on } \emptyset \)
** from **assms ** have ** \( \mathfrak{B} =\{\emptyset \} \)** using ** uniformity_base_props(5,6)
** with **\( \Phi \text{ is a uniformity on } \emptyset \) ** have ** \( False \)** using ** supersets_in_empty, unif_filter** unfolding ** IsFilter_def
** } **
** 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 \emptyset \)

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

** assumes **\( r \subseteq X\times X \), \( id(X) \subseteq r \)

Definition of IsUniformityBase:
\( \mathfrak{B} \text{ is a uniform base of } \Phi \equiv \mathfrak{B} \subseteq \Phi \wedge (\forall U\in \Phi .\ \exists B\in \mathfrak{B} .\ B\subseteq U) \)

Definition of Supersets:
\( \text{Supersets}(X,\mathcal{A} ) \equiv \{B\in Pow(X).\ \exists A\in \mathcal{A} .\ A\subseteq B\} \)

Definition of IsUniformityBaseOn:
\( \mathfrak{B} \text{ is a uniform base on } X \equiv \)
\( (\forall B_1\in \mathfrak{B} .\ \forall B_2\in \mathfrak{B} .\ \exists B_3\in \mathfrak{B} .\ B_3\subseteq B_1\cap B_2) \wedge (\forall B\in \mathfrak{B} .\ id(X)\subseteq B) \wedge \)
\( (\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)) \wedge (\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1) \wedge \)
\( \mathfrak{B} \subseteq Pow(X\times X) \wedge \mathfrak{B} \neq \emptyset \)

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

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)

** assumes **\( A\subseteq X \), \( A\in \mathcal{A} \)

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)

** assumes **\( \mathfrak{B} \text{ is a uniform base on } X \)