# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory UniformSpace_ZF imports Topology_ZF_2 Topology_ZF_4a
begin

This theory defines uniform spaces and proves their basic properties.

### Entourages and neighborhoods

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

shows $$\Phi \neq \emptyset$$ using assms unfolding IsUniformity_def, IsFilter_def

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

shows $$W\{x\} \neq \emptyset$$ and $$x \in W\{x\}$$proof
from assms(1,2) have $$id(X) \subseteq W$$ unfolding IsUniformity_def, IsFilter_def
with $$x\in X$$ show $$x\in W\{x\}$$ and $$W\{x\} \neq \emptyset$$
qed

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

lemma unif_filter:

assumes $$\Phi \text{ is a uniformity on } X$$

shows $$\Phi \text{ is a filter on } (X\times X)$$ using assms unfolding IsUniformity_def

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

shows $$A \subseteq X\times X$$, $$id(X) \subseteq A$$, $$\exists V\in \Phi .\ V\circ V \subseteq A$$, $$converse(A) \in \Phi$$proof
from assms show $$id(X) \subseteq A$$, $$\exists V\in \Phi .\ V\circ V \subseteq A$$, $$converse(A) \in \Phi$$ unfolding IsUniformity_def
from assms show $$A \subseteq X\times X$$ using unif_filter unfolding IsFilter_def
qed

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

shows $$\exists V\in \Phi .\ V\circ V \subseteq W \wedge V=converse(V)$$proof
from assms obtain $$U$$ where $$U\in \Phi$$ and $$U\circ U \subseteq W$$ unfolding IsUniformity_def
let $$V = U \cap converse(U)$$
from assms(1), $$U\in \Phi$$ have $$V \in \Phi$$ and $$V = converse(V)$$ unfolding IsUniformity_def, IsFilter_def
moreover
from $$U\circ U \subseteq W$$ have $$V\circ V \subseteq W$$
ultimately show $$thesis$$
qed

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

shows $$\exists B\in \Phi .\ B\circ (B\circ B) \subseteq A \wedge B=converse(B)$$proof
from assms obtain $$C$$ where $$C\in \Phi$$ and $$C\circ C \subseteq A$$ unfolding IsUniformity_def
from assms(1), $$C\in \Phi$$ obtain $$B$$ where $$B\in \Phi$$, $$B\circ B \subseteq C$$ and $$B=converse(B)$$ using half_size_symm
with $$C\circ C \subseteq A$$ have $$(B\circ B)\circ (B\circ B) \subseteq A$$
with assms(1), $$B\in \Phi$$ have $$B\circ (B\circ B) \subseteq A$$ using entourage_props(1,2)
with $$B\in \Phi$$, $$B=converse(B)$$ show $$thesis$$
qed

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

shows $$W \subseteq X\times X$$ and $$domain(W) = X$$proof
from assms show $$W \subseteq X\times X$$ unfolding IsUniformity_def, IsFilter_def
show $$domain(W) = X$$proof
from assms show $$domain(W) \subseteq X$$ unfolding IsUniformity_def, IsFilter_def
from assms show $$X \subseteq domain(W)$$ unfolding IsUniformity_def
qed
qed

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

shows $$W\{x\} \subseteq X$$ using assms, uni_domain(1)

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\}$$

shows $$\mathcal{M} :X\rightarrow Pow(Pow(X))$$ and $$\forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \}$$proof
from assms have $$\forall x\in X.\ \{V\{x\}.\ V\in \Phi \} \in Pow(Pow(X))$$ using IsUniformity_def, IsFilter_def, image_subset
with assms show $$\mathcal{M} :X\rightarrow Pow(Pow(X))$$ using ZF_fun_from_total
with assms show $$\forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \}$$ using ZF_fun_from_tot_val
qed

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\}$$

shows $$\mathcal{M} (x) \text{ is a filter on } X$$proof
from assms have PhiFilter: $$\Phi \text{ is a filter on } (X\times X)$$ and $$\mathcal{M} :X\rightarrow Pow(Pow(X))$$ and $$\mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \}$$ using IsUniformity_def, neigh_filt_fun
have $$\emptyset \notin \mathcal{M} (x)$$proof
from assms, $$x\in X$$ have $$\emptyset \notin \{V\{x\}.\ V\in \Phi \}$$ using neigh_not_empty
with $$\mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \}$$ show $$\emptyset \notin \mathcal{M} (x)$$
qed
moreover
have $$X \in \mathcal{M} (x)$$proof
note $$\mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \}$$
moreover
from assms have $$X\times X \in \Phi$$ unfolding IsUniformity_def, IsFilter_def
hence $$(X\times X)\{x\} \in \{V\{x\}.\ V\in \Phi \}$$
moreover
from $$x\in X$$ have $$(X\times X)\{x\} = X$$
ultimately show $$X \in \mathcal{M} (x)$$
qed
moreover
from $$\mathcal{M} :X\rightarrow Pow(Pow(X))$$, $$x\in X$$ have $$\mathcal{M} (x) \subseteq Pow(X)$$ using apply_funtype
moreover
have LargerIn: $$\forall B \in \mathcal{M} (x).\ \forall C \in Pow(X).\ B\subseteq C \longrightarrow C \in \mathcal{M} (x)$$proof
{
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
moreover
have $$\forall A \in \mathcal{M} (x).\ \forall B \in \mathcal{M} (x).\ A\cap B \in \mathcal{M} (x)$$proof
{
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
ultimately show $$thesis$$ unfolding IsFilter_def
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$$

shows $$\{V\{x\}.\ V\in \Phi \} \text{ is a filter on } X$$ using assms, filter_from_uniformity, ZF_fun_from_tot_val1

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

shows $$W \in \{V\{x\}.\ V\in \Phi \}$$ using assms, filter_from_uniformity, ZF_fun_from_tot_val1 unfolding IsFilter_def

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

shows $$\{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} \text{ is a neighborhood system on } X$$proof
let $$\mathcal{M} = \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\}$$
from assms have $$\mathcal{M} :X\rightarrow Pow(Pow(X))$$ and Mval: $$\forall x\in X.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \}$$ using IsUniformity_def, neigh_filt_fun
moreover
from assms have $$\forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X)$$ using filter_from_uniformity
moreover {
fix $$x$$
assume $$x\in X$$
have $$\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)))$$proof
{
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
{
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
ultimately show $$\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N \in \mathcal{M} (y))$$
qed
}
thus $$thesis$$
qed
} ultimately show $$thesis$$ unfolding IsNeighSystem_def
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:

shows $$\text{UniformTopology}(\Phi ,X) = \{U \in Pow(X).\ \forall x\in U.\ U \in \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\}(x)\}$$proof
let $$\mathcal{M} = \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\}$$
have $$\forall U\in Pow(X).\ \forall x\in U.\ \mathcal{M} (x) = \{V\{x\}.\ V\in \Phi \}$$ using ZF_fun_from_tot_val1
then show $$thesis$$ unfolding UniformTopology_def
qed

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, uniftop_def_alt, topology_from_neighs

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

shows $$\{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} = \text{ neighborhood system of } \text{UniformTopology}(\Phi ,X)$$ using assms, neigh_from_uniformity, nei_top_nei_round_trip, uniftop_def_alt

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

lemma uniftop_def_alt1:

assumes $$\Phi \text{ is a uniformity on } X$$

shows $$\text{UniformTopology}(\Phi ,X) = \{U\in Pow(X).\ \forall x\in U.\ \exists W\in \Phi .\ W\{x\} \subseteq U\}$$proof
let $$T = \text{UniformTopology}(\Phi ,X)$$
show $$T \subseteq \{U\in Pow(X).\ \forall x\in U.\ \exists W\in \Phi .\ W\{x\} \subseteq U\}$$ unfolding UniformTopology_def
{
fix $$U$$
assume $$U\in \{U\in Pow(X).\ \forall x\in U.\ \exists W\in \Phi .\ W\{x\} \subseteq U\}$$
then have $$U\in Pow(X)$$ and I: $$\forall x\in U.\ \exists W\in \Phi .\ W\{x\} \subseteq U$$
{
fix $$x$$
assume $$x\in U$$
with I obtain $$W$$ where $$W\in \Phi$$ and $$W\{x\} \subseteq U$$
let $$\mathfrak{F} = \{V\{x\}.\ V\in \Phi \}$$
from assms(1), $$U\in Pow(X)$$, $$x\in U$$, $$W\in \Phi$$ have $$\mathfrak{F} \text{ is a filter on } X$$ and $$W\{x\} \in \mathfrak{F}$$ using unif_filter_at_point
with $$U\in Pow(X)$$, $$W\{x\} \subseteq U$$ have $$U\in \mathfrak{F}$$ using is_filter_def_split(5)
}
hence $$\forall x\in U.\ U \in \{V\{x\}.\ V\in \Phi \}$$
with $$U\in Pow(X)$$ have $$U\in T$$ unfolding UniformTopology_def
}
thus $$\{U\in Pow(X).\ \forall x\in U.\ \exists W\in \Phi .\ W\{x\} \subseteq U\} \subseteq T$$
qed

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

shows $$V\{x\} \in \mathcal{M} (x)$$proof
from assms(1,4) have $$\mathcal{M} = \{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\}$$ using neigh_unif_same
with assms(2,3) show $$thesis$$ using ZF_fun_from_tot_val1
qed

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

shows $$\mathcal{S} \{x\} = \{W\{x\}.\ W\in \Phi \}$$proof
let $$T = \text{UniformTopology}(\Phi ,X)$$
let $$\mathcal{M} = \text{ neighborhood system of } T$$
from assms(1,2) have $$x \in \bigcup T$$ using uniform_top_is_top(2)
with assms(3) have $$\mathcal{M} (x) = \mathcal{S} \{x\}$$ using neigh_from_nei
moreover
from assms(1) have $$\mathcal{M} = \{\langle x,\{W\{x\}.\ W\in \Phi \}\rangle .\ x\in X\}$$ using neigh_unif_same
with assms(2) have $$\mathcal{M} (x) = \{W\{x\}.\ W\in \Phi \}$$ using ZF_fun_from_tot_val1
ultimately show $$thesis$$
qed

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

shows $$W\{x\} \in \mathcal{S} \{x\}$$ using assms, utopsnneip

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

shows $$\text{Closure}(R,J\times _tJ) \subseteq W\circ (R\circ W)$$proof
let $$M = \text{ set neighborhood system of } (J\times _tJ)$$
fix $$z$$
assume zMem: $$z \in \text{Closure}(R,J\times _tJ)$$
from assms(1,5) have Jtop: $$J \text{ is a topology }$$ and $$\bigcup J = X$$ using uniform_top_is_top
then have JJtop: $$(J\times _tJ) \text{ is a topology }$$ and JxJ: $$\bigcup (J\times _tJ) = X\times X$$ using Top_1_4_T1(1,3)
with assms(2) have $$topology0(J\times _tJ)$$ and $$R \subseteq \bigcup (J\times _tJ)$$ unfolding topology0_def
then have $$\text{Closure}(R,J\times _tJ) \subseteq \bigcup (J\times _tJ)$$ using Top_3_L11(1)
with $$z \in \text{Closure}(R,J\times _tJ)$$, JxJ have $$z\in X\times X$$
let $$x = \text{fst}(z)$$
let $$y = \text{snd}(z)$$
from $$z\in X\times X$$ have $$x\in X$$, $$y\in X$$, $$z = \langle x,y\rangle$$
with assms(1,3,5), Jtop have $$(W\{x\})\times (W\{y\}) \in M(\{x\}\times \{y\})$$ using utopsnnei, neitx
moreover
from $$z = \langle x,y\rangle$$ have $$\{x\}\times \{y\} = \{z\}$$ by (rule pair_prod )
ultimately have $$(W\{x\})\times (W\{y\}) \in M\{z\}$$
with zMem, JJtop, $$R \subseteq \bigcup (J\times _tJ)$$ have $$(W\{x\})\times (W\{y\}) \cap R \neq \emptyset$$ using neindisj
with assms(4) have $$\langle x,y\rangle \in W\circ (R\circ W)$$ using sym_rel_comp
with $$z = \langle x,y\rangle$$ show $$z \in W\circ (R\circ W)$$
qed

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

theorem utopreg:

assumes $$\Phi \text{ is a uniformity on } X$$

shows $$\text{UniformTopology}(\Phi ,X) \text{ is regular }$$proof
let $$J = \text{UniformTopology}(\Phi ,X)$$
let $$\mathcal{S} = \text{ set neighborhood system of } J$$
from assms have $$\bigcup J = X$$ and Jtop: $$J \text{ is a topology }$$ and cntx: $$topology0(J)$$ using uniform_top_is_top unfolding topology0_def
have $$\forall U\in J.\ \forall x\in U.\ \exists V\in J.\ x\in V \wedge \text{Closure}(V,J)\subseteq U$$proof
{
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
with Jtop show $$J \text{ is regular }$$ using is_regular_def_alt
qed

### Base of a uniformity

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

shows $$\{V\in \Phi .\ V = converse(V)\} \text{ is a uniform base of } \Phi$$proof
let $$\mathfrak{B} = \{V\in \Phi .\ V = converse(V)\}$$
{
fix $$W$$
assume $$W\in \Phi$$
with assms obtain $$V$$ where $$V\in \Phi$$, $$V\circ V \subseteq W$$, $$V=converse(V)$$ using half_size_symm
from assms, $$V\in \Phi$$ have $$V \subseteq V\circ V$$ using entourage_props(1,2), refl_square_greater
with $$V\circ V \subseteq W$$, $$V\in \Phi$$, $$V=converse(V)$$ have $$\exists V\in \mathfrak{B} .\ V\subseteq W$$
}
hence $$\forall W\in \Phi .\ \exists V\in \mathfrak{B} .\ V \subseteq W$$
then show $$thesis$$ unfolding IsUniformityBase_def
qed

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

shows $$\Phi = \text{Supersets}(X\times X,\mathfrak{B} )$$proof
from assms show $$\Phi \subseteq \text{Supersets}(X\times X,\mathfrak{B} )$$ unfolding IsUniformityBase_def, Supersets_def using entourage_props(1)
from assms show $$\text{Supersets}(X\times X,\mathfrak{B} ) \subseteq \Phi$$ unfolding Supersets_def, IsUniformityBase_def, IsUniformity_def, IsFilter_def
qed

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

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$ using assms unfolding IsUniformityBaseOn_def

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

shows $$\mathfrak{B} \text{ is a uniform base on } X$$proof
let $$\Phi = \text{Supersets}(X\times X,\mathfrak{B} )$$
have $$\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$$proof
{
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
moreover
have $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$proof
{
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
moreover
have $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$proof
{
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
moreover
have $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$proof
{
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
moreover
from assms(2) have $$\mathfrak{B} \neq \emptyset$$ using supersets_of_empty, uniformity_non_empty
ultimately show $$\mathfrak{B} \text{ is a uniform base on } X$$ unfolding IsUniformityBaseOn_def using assms(1)
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$$

shows $$\text{Supersets}(X\times X,\mathfrak{B} ) \text{ is a uniformity on } X$$proof
let $$\Phi = \text{Supersets}(X\times X,\mathfrak{B} )$$
from assms(2) have $$\mathfrak{B} \subseteq Pow(X\times X)$$ using uniformity_base_props(5)
have $$\Phi \text{ is a filter on } (X\times X)$$proof
from assms have $$\emptyset \notin \Phi$$ unfolding Supersets_def using uniformity_base_props(2)
moreover
have $$X\times X \in \Phi$$proof
from assms(2) obtain $$B$$ where $$B\in \mathfrak{B}$$ using uniformity_base_props(6)
with $$\mathfrak{B} \subseteq Pow(X\times X)$$ show $$X\times X \in \Phi$$ unfolding Supersets_def
qed
moreover
have $$\Phi \subseteq Pow(X\times X)$$ unfolding Supersets_def
moreover
have $$\forall U\in \Phi .\ \forall V\in \Phi .\ U\cap V \in \Phi$$proof
{
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
moreover
have $$\forall U\in \Phi .\ \forall C\in Pow(X\times X).\ U\subseteq C \longrightarrow C\in \Phi$$proof
{
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
ultimately show $$\Phi \text{ is a filter on } (X\times X)$$ unfolding IsFilter_def
qed
moreover
have $$\forall U\in \Phi .\ id(X) \subseteq U \wedge (\exists V\in \Phi .\ V\circ V \subseteq U) \wedge converse(U) \in \Phi$$proof
{
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
ultimately show $$thesis$$ unfolding IsUniformity_def
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$$

shows $$\neg ( \text{Supersets}(\emptyset \times \emptyset ,\mathfrak{B} ) \text{ is a uniformity on } \emptyset )$$proof
{
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
end
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} )$$
lemma unif_filter:

assumes $$\Phi \text{ is a uniformity on } X$$

shows $$\Phi \text{ is a filter on } (X\times X)$$
lemma half_size_symm:

assumes $$\Phi \text{ is a uniformity on } X$$, $$W\in \Phi$$

shows $$\exists V\in \Phi .\ V\circ V \subseteq W \wedge V=converse(V)$$
lemma entourage_props:

assumes $$\Phi \text{ is a uniformity on } X$$ and $$A\in \Phi$$

shows $$A \subseteq X\times X$$, $$id(X) \subseteq A$$, $$\exists V\in \Phi .\ V\circ V \subseteq A$$, $$converse(A) \in \Phi$$
lemma uni_domain:

assumes $$\Phi \text{ is a uniformity on } X$$, $$W\in \Phi$$

shows $$W \subseteq X\times X$$ and $$domain(W) = X$$
lemma ZF_fun_from_total:

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

shows $$\{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y$$
lemma ZF_fun_from_tot_val:

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

shows $$f(x) = b(x)$$ and $$b(x)\in Y$$
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 \}$$
lemma neigh_not_empty:

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

shows $$W\{x\} \neq \emptyset$$ and $$x \in W\{x\}$$
lemma image_greater_rel:

assumes $$x \in U\{x\}$$ and $$U\{x\} \subseteq C$$

shows $$(U \cup C\times C)\{x\} = C$$
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$$
lemma ZF_fun_from_tot_val1:

assumes $$x\in X$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\}(x)=b(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 \}\}$$
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$$
lemma uniftop_def_alt: shows $$\text{UniformTopology}(\Phi ,X) = \{U \in Pow(X).\ \forall x\in U.\ U \in \{\langle t,\{V\{t\}.\ V\in \Phi \}\rangle .\ t\in X\}(x)\}$$
theorem topology_from_neighs:

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$$
theorem nei_top_nei_round_trip:

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 $$(\text{ neighborhood system of } T) = \mathcal{M}$$
lemma unif_filter_at_point:

assumes $$\Phi \text{ is a uniformity on } X$$ and $$x\in X$$

shows $$\{V\{x\}.\ V\in \Phi \} \text{ is a filter on } X$$
lemma is_filter_def_split:

assumes $$\mathfrak{F} \text{ is a filter on } X$$

shows $$0\notin \mathfrak{F}$$, $$X\in \mathfrak{F}$$, $$\mathfrak{F} \subseteq Pow(X)$$, $$\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F}$$ and $$\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F}$$
theorem neigh_unif_same:

assumes $$\Phi \text{ is a uniformity on } X$$

shows $$\{\langle x,\{V\{x\}.\ V\in \Phi \}\rangle .\ x\in X\} = \text{ neighborhood system of } \text{UniformTopology}(\Phi ,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$$
lemma neigh_from_nei:

assumes $$x\in \bigcup T$$

shows $$(\text{ neighborhood system of } T)(x) = (\text{ set neighborhood system of } T)\{x\}$$
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)$$

shows $$\mathcal{S} \{x\} = \{W\{x\}.\ W\in \Phi \}$$
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$$
theorem Top_1_4_T1:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$

shows $$(T\times _tS) \text{ is a topology }$$, $$\text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS)$$, $$\bigcup (T\times _tS) = \bigcup T \times \bigcup S$$
lemma (in topology0) Top_3_L11:

assumes $$A \subseteq \bigcup T$$

shows $$cl(A) \subseteq \bigcup T$$, $$cl(\bigcup T - A) = \bigcup T - int(A)$$
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)$$

shows $$W\{x\} \in \mathcal{S} \{x\}$$
lemma neitx:

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

shows $$A\times B \in (\text{ set neighborhood system of } (T\times _tS))(C\times D)$$
lemma pair_prod:

assumes $$z = \langle x,y\rangle$$

shows $$\{x\}\times \{y\} = \{z\}$$
lemma neindisj:

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\}$$

shows $$N\cap A \neq 0$$
lemma sym_rel_comp:

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

shows $$\langle x,y\rangle \in (W\circ (R\circ W))$$
corollary open_nei_singl:

assumes $$V\in T$$, $$x\in V$$

shows $$V \in (\text{ set neighborhood system of } T)\{x\}$$
lemma ustex3sym:

assumes $$\Phi \text{ is a uniformity on } X$$, $$A\in \Phi$$

shows $$\exists B\in \Phi .\ B\circ (B\circ B) \subseteq A \wedge B=converse(B)$$
lemma ustimasn:

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

shows $$W\{x\} \subseteq X$$
lemma neii2:

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

shows $$\exists U\in T.\ (A\subseteq U \wedge U\subseteq N)$$
lemma entourage_props:

assumes $$\Phi \text{ is a uniformity on } X$$ and $$A\in \Phi$$

shows $$A \subseteq X\times X$$, $$id(X) \subseteq A$$, $$\exists V\in \Phi .\ V\circ V \subseteq A$$, $$converse(A) \in \Phi$$
lemma (in topology0) top_closure_mono:

assumes $$B \subseteq \bigcup T$$ and $$A\subseteq B$$

shows $$cl(A) \subseteq cl(B)$$
lemma imasncls:

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

shows $$\text{Closure}(R\{x\},S) \subseteq \text{Closure}(R,T\times _tS)\{x\}$$
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)$$

shows $$\text{Closure}(R,J\times _tJ) \subseteq W\circ (R\circ W)$$
lemma is_regular_def_alt:

assumes $$T \text{ is a topology }$$

shows $$T \text{ is regular } \longleftrightarrow (\forall W\in T.\ \forall x\in W.\ \exists V\in T.\ x\in V \wedge \text{Closure}(V,T)\subseteq W)$$
lemma refl_square_greater:

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

shows $$r \subseteq r\circ 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$$
lemma supersets_of_empty: shows $$\text{Supersets}(X,\emptyset ) = \emptyset$$
lemma uniformity_non_empty:

assumes $$\Phi \text{ is a uniformity on } X$$

shows $$\Phi \neq \emptyset$$
lemma uniformity_base_props:

assumes $$\mathfrak{B} \text{ is a uniform base on } X$$

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$
lemma uniformity_base_props:

assumes $$\mathfrak{B} \text{ is a uniform base on } X$$

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$
lemma uniformity_base_props:

assumes $$\mathfrak{B} \text{ is a uniform base on } X$$

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$
lemma uniformity_base_props:

assumes $$\mathfrak{B} \text{ is a uniform base on } X$$

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$
lemma uniformity_base_props:

assumes $$\mathfrak{B} \text{ is a uniform base on } X$$

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$
lemma superset_gen:

assumes $$A\subseteq X$$, $$A\in \mathcal{A}$$

shows $$A \in \text{Supersets}(X,\mathcal{A} )$$
lemma uniformity_base_props:

assumes $$\mathfrak{B} \text{ is a uniform base on } X$$

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$
lemma uniformity_base_props:

assumes $$\mathfrak{B} \text{ is a uniform base on } X$$

shows $$\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$$, $$\forall B\in \mathfrak{B} .\ id(X)\subseteq B$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)$$, $$\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1$$, $$\mathfrak{B} \subseteq Pow(X\times X)$$ and $$\mathfrak{B} \neq \emptyset$$
lemma supersets_in_empty: shows $$\text{Supersets}(\emptyset ,\{\emptyset \}) = \{\emptyset \}$$