IsarMathLib

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

theory UniformSpace_ZF_2 imports UniformSpace_ZF
begin

The UniformSpace_ZF theory defines uniform spaces based on entourages (also called surroundings sometimes). In this theory we consider alternative definitions based of the notion of uniform covers and pseudometrics.

Uniform covers

Given a set \(X\) we can consider collections of subsets of \(X\) whose unions are equal to \(X\). Any such collection is called a cover of \(X\). We can define relation on the set of covers of \(X\), called "star refinement" (definition below). A collection of covers is a "family of uniform covers" if it is a filter with respect to the start refinement ordering. A member of such family is called a "uniform cover", but one has to remember that this notion has meaning only in the contexts a the whole family of uniform covers. Looking at a specific cover in isolation we can not say whether it is a uniform cover or not.

The set of all covers of \(X\) is called \( \text{Covers}(X) \).

definition

\( \text{Covers}(X) \equiv \{P \in Pow(Pow(X)).\ \bigcup P = X\} \)

A cover of a nonempty set must have a nonempty member.

lemma cover_nonempty:

assumes \( X\neq 0 \), \( P \in \text{Covers}(X) \)

shows \( \exists U\in P.\ U\neq 0 \) using assms unfolding Covers_def

A "star" of \(R\) with respect to \(\mathcal{R}\) is the union of all \(S\in \mathcal{R}\) that intersect \(R\).

definition

\( \text{Star}(R,\mathcal{R} ) \equiv \bigcup \{S\in \mathcal{R} .\ S\cap R \neq 0\} \)

An element of \(\mathcal{R}\) is a subset of its star with respect to \(\mathcal{R}\).

lemma element_subset_star:

assumes \( U\in P \)

shows \( U \subseteq \text{Star}(U,P) \) using assms unfolding Star_def

An alternative formula for star of a singleton.

lemma star_singleton:

shows \( (\bigcup \{V\times V.\ V\in P\})\{x\} = \text{Star}(\{x\},P) \) unfolding Star_def

Star of a larger set is larger.

lemma star_mono:

assumes \( U\subseteq V \)

shows \( \text{Star}(U,P) \subseteq \text{Star}(V,P) \) using assms unfolding Star_def

In particular, star of a set is larger than star of any singleton in that set.

corollary star_single_mono:

assumes \( x\in U \)

shows \( \text{Star}(\{x\},P) \subseteq \text{Star}(U,P) \) using assms, star_mono

A cover \(\mathcal{R}\) (of \(X\)) is said to be a "barycentric refinement" of a cover \(\mathcal{C}\) iff for every \(x\in X\) the star of \(\{x\}\) in \(\mathcal{R}\) is contained in some \(C\in \mathcal{C}\).

definition

\( P \lt ^B Q \equiv \forall x\in \bigcup P.\ \exists U\in Q.\ \text{Star}(\{x\},P) \subseteq U \)

A cover is a barycentric refinement of the collection of stars of the singletons \(\{x \}\) as \(x\) ranges over \(X\).

lemma singl_star_bary:

assumes \( P \in \text{Covers}(X) \)

shows \( P \lt ^B \{ \text{Star}(\{x\},P).\ x\in X\} \) using assms unfolding Covers_def, IsBarycentricRefinement_def

A cover \(\mathcal{R}\) is a "star refinement" of a cover \(\mathcal{C}\) iff for each \(R\in \mathcal{R}\) there is a \(C\in \mathcal{C}\) such that the star of \(R\) with respect to \(\mathcal{R}\) is contained in \(C\).

definition

\( P \lt ^* Q \equiv \forall U\in P.\ \exists V\in Q.\ \text{Star}(U,P) \subseteq V \)

Every cover star-refines the trivial cover \(\{ X\}\).

lemma cover_stref_triv:

assumes \( P \in \text{Covers}(X) \)

shows \( P \lt ^* \{X\} \) using assms unfolding Star_def, IsStarRefinement_def, Covers_def

Star refinement implies barycentric refinement.

lemma star_is_bary:

assumes \( Q\in \text{Covers}(X) \) and \( Q \lt ^* P \)

shows \( Q \lt ^B P \)proof
from assms(1) have \( \bigcup Q = X \) unfolding Covers_def
{
fix \( x \)
assume \( x\in X \)
with \( \bigcup Q = X \) obtain \( R \) where \( R\in Q \) and \( x\in R \)
with assms(2) obtain \( U \) where \( U\in P \) and \( \text{Star}(R,Q) \subseteq U \) unfolding IsStarRefinement_def
from \( x\in R \), \( \text{Star}(R,Q) \subseteq U \) have \( \text{Star}(\{x\},Q) \subseteq U \) using star_single_mono
with \( U\in P \) have \( \exists U\in P.\ \text{Star}(\{x\},Q) \subseteq U \)
}
with \( \bigcup Q = X \) show \( thesis \) unfolding IsBarycentricRefinement_def
qed

Barycentric refinement of a barycentric refinement is a star refinement.

lemma bary_bary_star:

assumes \( P\in \text{Covers}(X) \), \( Q\in \text{Covers}(X) \), \( R\in \text{Covers}(X) \), \( P \lt ^B Q \), \( Q \lt ^B R \), \( X\neq 0 \)

shows \( P \lt ^* R \)proof
{
fix \( U \)
assume \( U\in P \)
{
assume \( U = 0 \)
then have \( \text{Star}(U,P) = 0 \) unfolding Star_def
from assms(6,3) obtain \( V \) where \( V\in R \) using cover_nonempty
with \( \text{Star}(U,P) = 0 \) have \( \exists V\in R.\ \text{Star}(U,P) \subseteq V \)
}
moreover {
assume \( U\neq 0 \)
then obtain \( x_0 \) where \( x_0\in U \)
with assms(1,2,5), \( U\in P \) obtain \( V \) where \( V\in R \) and \( \text{Star}(\{x_0\},Q) \subseteq V \) unfolding Covers_def, IsBarycentricRefinement_def
have \( \text{Star}(U,P) \subseteq V \)proof
{
fix \( W \)
assume \( W\in P \) and \( W\cap U \neq 0 \)
from \( W\cap U \neq 0 \) obtain \( x \) where \( x\in W\cap U \)
with assms(2), \( U\in P \) have \( x\in \bigcup P \)
with assms(4) obtain \( C \) where \( C\in Q \) and \( \text{Star}(\{x\},P) \subseteq C \) unfolding IsBarycentricRefinement_def
with \( U\in P \), \( W\in P \), \( x\in W\cap U \), \( x_0\in U \), \( \text{Star}(\{x_0\},Q) \subseteq V \) have \( W\subseteq V \) unfolding Star_def
}
then show \( \text{Star}(U,P) \subseteq V \) unfolding Star_def
qed
with \( V\in R \) have \( \exists V\in R.\ \text{Star}(U,P) \subseteq V \)
} ultimately have \( \exists V\in R.\ \text{Star}(U,P) \subseteq V \)
}
then show \( P \lt ^* R \) unfolding IsStarRefinement_def
qed

The notion of a filter defined in Topology_ZF_4 is not sufficiently general to use it to define uniform covers, so we write the conditions directly. A nonempty collection \(\Theta\) of covers of \(X\) is a family of uniform covers if a) if \(\mathcal{R} \in \Theta\) and \(\mathcal{C}\) is any cover of \(X\) such that \(\mathcal{R}\) is a star refinement of \(\mathcal{C}\), then \(\mathcal{C} \in \Theta\). b) For any \(\mathcal{C},\mathcal{D} \in \Theta\) there is some \(\mathcal{R}\in\Theta\) such that \(\mathcal{R}\) is a star refinement of both \(\mathcal{C}\) and \(\mathcal{R}\).

This departs slightly from the definition in Wikipedia that requires that \(\Theta\) contains the trivial cover \(\{ X\}\). As we show in lemma unicov_contains_trivial below we don't loose anything by weakening the definition this way.

definition

\( \Theta \text{ are uniform covers of } X \equiv \Theta \subseteq \text{Covers}(X) \wedge \Theta \neq 0 \wedge \) \( (\forall \mathcal{R} \in \Theta .\ \forall \mathcal{C} \in \text{Covers}(X).\ ((\mathcal{R} \lt ^* \mathcal{C} ) \longrightarrow \mathcal{C} \in \Theta )) \wedge \) \( (\forall \mathcal{C} \in \Theta .\ \forall \mathcal{D} \in \Theta .\ \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^* \mathcal{C} ) \wedge (\mathcal{R} \lt ^* \mathcal{D} )) \)

A family of uniform covers contain the trivial cover \(\{ X\}\).

lemma unicov_contains_triv:

assumes \( \Theta \text{ are uniform covers of } X \)

shows \( \{X\} \in \Theta \)proof
from assms obtain \( \mathcal{R} \) where \( \mathcal{R} \in \Theta \) unfolding AreUniformCovers_def
with assms show \( thesis \) using cover_stref_triv unfolding AreUniformCovers_def, Covers_def
qed

If \(\Theta\) are uniform covers of \(X\) then we can recover \(X\) from \(\Theta\) by taking \(\bigcup\bigcup \Theta\).

lemma space_from_unicov:

assumes \( \Theta \text{ are uniform covers of } X \)

shows \( X = \bigcup \bigcup \Theta \)proof
from assms show \( X \subseteq \bigcup \bigcup \Theta \) using unicov_contains_triv unfolding AreUniformCovers_def
from assms show \( \bigcup \bigcup \Theta \subseteq X \) unfolding AreUniformCovers_def, Covers_def
qed

Every uniform cover has a star refinement.

lemma unicov_has_star_ref:

assumes \( \Theta \text{ are uniform covers of } X \) and \( P\in \Theta \)

shows \( \exists Q\in \Theta .\ (Q \lt ^* P) \) using assms unfolding AreUniformCovers_def

In particular, every uniform cover has a barycentric refinement.

corollary unicov_has_bar_ref:

assumes \( \Theta \text{ are uniform covers of } X \) and \( P\in \Theta \)

shows \( \exists Q\in \Theta .\ (Q \lt ^B P) \)proof
from assms obtain \( Q \) where \( Q\in \Theta \) and \( Q \lt ^* P \) using unicov_has_star_ref
with assms show \( thesis \) unfolding AreUniformCovers_def using star_is_bary
qed

From the definition of uniform covers we know that if a uniform cover \(P\) is a star-refinement of a cover \(Q\) then \(Q\) is in a uniform cover. The next lemma shows that in order for \(Q\) to be a uniform cover it is sufficient that \(P\) is a barycentric refinement of \(Q\).

lemma unicov_bary_cov:

assumes \( \Theta \text{ are uniform covers of } X \), \( P\in \Theta \), \( Q \in \text{Covers}(X) \), \( P \lt ^B Q \) and \( X\neq 0 \)

shows \( Q\in \Theta \)proof
from assms(1,2) obtain \( R \) where \( R\in \Theta \) and \( R \lt ^B P \) using unicov_has_bar_ref
from assms(1,2,3), \( R\in \Theta \) have \( P \in \text{Covers}(X) \), \( Q \in \text{Covers}(X) \), \( R \in \text{Covers}(X) \) unfolding AreUniformCovers_def
with assms(1,3,4,5), \( R\in \Theta \), \( R \lt ^B P \) show \( thesis \) using bary_bary_star unfolding AreUniformCovers_def
qed

A technical lemma to simplify proof of the uniformity_from_unicov theorem.

lemma star_ref_mem:

assumes \( U\in P \), \( P \lt ^*Q \) and \( \bigcup \{W\times W.\ W\in Q\} \subseteq A \)

shows \( U\times U \subseteq A \)proof
from assms(1,2) obtain \( W \) where \( W\in Q \) and \( \bigcup \{S\in P.\ S\cap U \neq 0\} \subseteq W \) unfolding IsStarRefinement_def, Star_def
with assms(1,3) show \( U\times U \subseteq A \)
qed

An identity related to square (in the sense of composition) of a relation of the form \(\bigcup \{U\times U : U\in P\}\). I am amazed that Isabelle can see that this is true without an explicit proof, I can't.

lemma rel_square_starr:

shows \( (\bigcup \{U\times U.\ U\in P\})\circ (\bigcup \{U\times U.\ U\in P\}) = \bigcup \{U\times \text{Star}(U,P).\ U\in P\} \) unfolding Star_def

An identity similar to rel_square_starr but with Star on the left side of the Cartesian product:

lemma rel_square_starl:

shows \( (\bigcup \{U\times U.\ U\in P\})\circ (\bigcup \{U\times U.\ U\in P\}) = \bigcup \{ \text{Star}(U,P)\times U.\ U\in P\} \) unfolding Star_def

A somewhat technical identity about the square of a symmetric relation:

lemma rel_sq_image:

assumes \( W = converse(W) \), \( domain(W) \subseteq X \)

shows \( \text{Star}(\{x\},\{W\{t\}.\ t\in X\}) = (W\circ W)\{x\} \)proof
have I: \( \text{Star}(\{x\},\{W\{t\}.\ t\in X\}) = \bigcup \{S\in \{W\{t\}.\ t\in X\}.\ x\in S\} \) unfolding Star_def
{
fix \( y \)
assume \( y \in \text{Star}(\{x\},\{W\{t\}.\ t\in X\}) \)
with I obtain \( S \) where \( y\in S \), \( x\in S \), \( S \in \{W\{t\}.\ t\in X\} \)
from \( S \in \{W\{t\}.\ t\in X\} \) obtain \( t \) where \( t\in X \) and \( S = W\{t\} \)
with \( x\in S \), \( y\in S \) have \( \langle t,x\rangle \in W \) and \( \langle t,y\rangle \in W \)
from \( \langle t,x\rangle \in W \) have \( \langle x,t\rangle \in converse(W) \)
with assms(1), \( \langle t,y\rangle \in W \) have \( y \in (W\circ W)\{x\} \) using rel_compdef
}
then show \( \text{Star}(\{x\},\{W\{t\}.\ t\in X\}) \subseteq (W\circ W)\{x\} \)
{
fix \( y \)
assume \( y\in (W\circ W)\{x\} \)
then obtain \( t \) where \( \langle x,t\rangle \in W \) and \( \langle t,y\rangle \in W \) using rel_compdef
from assms(2), \( \langle t,y\rangle \in W \) have \( t\in X \)
from \( \langle x,t\rangle \in W \) have \( \langle t,x\rangle \in converse(W) \)
with assms(1), I, \( \langle t,y\rangle \in W \), \( t\in X \) have \( y \in \text{Star}(\{x\},\{W\{t\}.\ t\in X\}) \)
}
then show \( (W\circ W)\{x\} \subseteq \text{Star}(\{x\},\{W\{t\}.\ t\in X\}) \)
qed

Given a family of uniform covers of \(X\) we can create a uniformity on \(X\) by taking the supersets of \(\bigcup \{A\times A: A\in P \}\) as \(P\) ranges over the uniform covers. The next definition specifies the operation creating entourages from uniform covers.

definition

\( \text{UniformityFromUniCov}(X,\Theta ) \equiv \text{Supersets}(X\times X,\{\bigcup \{U\times U.\ U\in P\}.\ P\in \Theta \}) \)

For any member \(P\) of a cover \(\Theta\) the set \(\bigcup \{U\times U : U\in P\}\) is a member of \( \text{UniformityFromUniCov}(X,\Theta ) \).

lemma basic_unif:

assumes \( \Theta \subseteq \text{Covers}(X) \), \( P\in \Theta \)

shows \( \bigcup \{U\times U.\ U\in P\} \in \text{UniformityFromUniCov}(X,\Theta ) \) using assms unfolding UniformityFromUniCov_def, Supersets_def, Covers_def

If \(\Theta\) is a family of uniform covers of \(X\) then \( \text{UniformityFromUniCov}(X,\Theta ) \) is a uniformity on \(X\)

theorem uniformity_from_unicov:

assumes \( \Theta \text{ are uniform covers of } X \), \( X\neq 0 \)

shows \( \text{UniformityFromUniCov}(X,\Theta ) \text{ is a uniformity on } X \)proof
let \( \Phi = \text{UniformityFromUniCov}(X,\Theta ) \)
have \( \Phi \text{ is a filter on } (X\times X) \)proof
have \( 0 \notin \Phi \)proof
{
assume \( 0 \in \Phi \)
then obtain \( P \) where \( P\in \Theta \) and \( 0 = \bigcup \{U\times U.\ U\in P\} \) unfolding UniformityFromUniCov_def, Supersets_def
hence \( \bigcup P = 0 \)
with assms, \( P\in \Theta \) have \( False \) unfolding AreUniformCovers_def, Covers_def
}
thus \( thesis \)
qed
moreover
have \( X\times X \in \Phi \)proof
from assms have \( X\times X \in \{\bigcup \{U\times U.\ U\in P\}.\ P\in \Theta \} \) using unicov_contains_triv unfolding AreUniformCovers_def
then show \( thesis \) unfolding Supersets_def, UniformityFromUniCov_def
qed
moreover
have \( \Phi \subseteq Pow(X\times X) \) unfolding UniformityFromUniCov_def, Supersets_def
moreover
have \( \forall A\in \Phi .\ \forall B\in \Phi .\ A\cap B \in \Phi \)proof
{
fix \( A \) \( B \)
assume \( A\in \Phi \), \( B\in \Phi \)
then have \( A\cap B \subseteq X\times X \) unfolding UniformityFromUniCov_def, Supersets_def
from \( A\in \Phi \), \( B\in \Phi \) obtain \( P_A \) \( P_B \) where \( P_A\in \Theta \), \( P_B\in \Theta \) and I: \( \bigcup \{U\times U.\ U\in P_A\} \subseteq A \), \( \bigcup \{U\times U.\ U\in P_B\} \subseteq B \) unfolding UniformityFromUniCov_def, Supersets_def
from assms(1), \( P_A\in \Theta \), \( P_B\in \Theta \) obtain \( P \) where \( P\in \Theta \) and \( P \lt ^*P_A \) and \( P \lt ^*P_B \) unfolding AreUniformCovers_def
have \( \bigcup \{U\times U.\ U\in P\} \subseteq A\cap B \)proof
{
fix \( U \)
assume \( U\in P \)
with \( P \lt ^*P_A \), \( P \lt ^*P_B \), I have \( U\times U \subseteq A \) and \( U\times U \subseteq B \) using star_ref_mem
}
thus \( thesis \)
qed
with \( A\cap B \subseteq X\times X \), \( P\in \Theta \) have \( A\cap B \in \Phi \) unfolding Supersets_def, UniformityFromUniCov_def
}
thus \( thesis \)
qed
moreover
have \( \forall B\in \Phi .\ \forall C\in Pow(X\times X).\ B\subseteq C \longrightarrow C\in \Phi \)proof
{
fix \( B \) \( C \)
assume \( B\in \Phi \), \( C\in Pow(X\times X) \), \( B\subseteq C \)
from \( B\in \Phi \) obtain \( P_B \) where \( \bigcup \{U\times U.\ U\in P_B\} \subseteq B \), \( P_B\in \Theta \) unfolding UniformityFromUniCov_def, Supersets_def
with \( C\in Pow(X\times X) \), \( B\subseteq C \) have \( C\in \Phi \) unfolding UniformityFromUniCov_def, Supersets_def
}
thus \( thesis \)
qed
ultimately show \( thesis \) unfolding IsFilter_def
qed
moreover
have \( \forall A\in \Phi .\ id(X) \subseteq A \wedge (\exists B\in \Phi .\ B\circ B \subseteq A) \wedge converse(A) \in \Phi \)proof
fix \( A \)
assume \( A\in \Phi \)
then obtain \( P \) where \( \bigcup \{U\times U.\ U\in P\} \subseteq A \), \( P\in \Theta \) unfolding UniformityFromUniCov_def, Supersets_def
have \( id(X)\subseteq A \)proof
from assms(1), \( P\in \Theta \) have \( \bigcup P = X \) unfolding AreUniformCovers_def, Covers_def
with \( \bigcup \{U\times U.\ U\in P\} \subseteq A \) show \( thesis \)
qed
moreover
have \( \exists B\in \Phi .\ B\circ B \subseteq A \)proof
from assms(1), \( P\in \Theta \) have \( \bigcup \{U\times U.\ U\in P\} \in \Phi \) unfolding AreUniformCovers_def, Covers_def, UniformityFromUniCov_def, Supersets_def
from assms(1), \( P\in \Theta \) obtain \( Q \) where \( Q\in \Theta \) and \( Q \lt ^* P \) using unicov_has_star_ref
let \( B = \bigcup \{U\times U.\ U\in Q\} \)
from assms(1), \( Q\in \Theta \) have \( B \in \Phi \) unfolding AreUniformCovers_def, Covers_def, UniformityFromUniCov_def, Supersets_def
moreover
have \( B\circ B \subseteq A \)proof
have II: \( B\circ B = \bigcup \{U\times \text{Star}(U,Q).\ U\in Q\} \) using rel_square_starr
have \( \forall U\in Q.\ \exists V\in P.\ U\times \text{Star}(U,Q) \subseteq V\times V \)proof
fix \( U \)
assume \( U\in Q \)
with \( Q \lt ^* P \) obtain \( V \) where \( V\in P \) and \( \text{Star}(U,Q) \subseteq V \) unfolding IsStarRefinement_def
with \( U\in Q \) have \( V\in P \) and \( U\times \text{Star}(U,Q) \subseteq V\times V \) using element_subset_star
thus \( \exists V\in P.\ U\times \text{Star}(U,Q) \subseteq V\times V \)
qed
hence \( \bigcup \{U\times \text{Star}(U,Q).\ U\in Q\} \subseteq \bigcup \{V\times V.\ V\in P\} \)
with \( \bigcup \{V\times V.\ V\in P\} \subseteq A \) have \( \bigcup \{U\times \text{Star}(U,Q).\ U\in Q\} \subseteq A \)
with II show \( thesis \)
qed
ultimately show \( thesis \)
qed
moreover
from \( A\in \Phi \), \( P\in \Theta \), \( \bigcup \{U\times U.\ U\in P\} \subseteq A \) have \( converse(A) \in \Phi \) unfolding AreUniformCovers_def, UniformityFromUniCov_def, Supersets_def
ultimately show \( id(X) \subseteq A \wedge (\exists B\in \Phi .\ B\circ B \subseteq A) \wedge converse(A) \in \Phi \)
qed
ultimately show \( \Phi \text{ is a uniformity on } X \) unfolding IsUniformity_def
qed

Given a uniformity \(\Phi\) on \(X\) we can create a family of uniform covers by taking the collection of covers \(P\) for which there exist an entourage \(U\in \Phi\) such that for each \(x\in X\), there is an \(A\in P\) such that \(U(\{ x\}) \subseteq A\). The next definition specifies the operation of creating a family of uniform covers from a uniformity.

definition

\( \text{UniCovFromUniformity}(X,\Phi ) \equiv \{P\in \text{Covers}(X).\ \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A\} \)

When we convert the quantifiers into unions and intersections in the definition of UniCovFromUniformity we get an alternative definition of the operation that creates a family of uniform covers from a uniformity. Just a curiosity, not used anywhere.

lemma UniCovFromUniformityDef:

assumes \( X\neq 0 \)

shows \( \text{UniCovFromUniformity}(X,\Phi ) = (\bigcup U\in \Phi .\ \bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \)proof
have \( \{P\in \text{Covers}(X).\ \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A\} = \) \( (\bigcup U\in \Phi .\ \bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \)proof
{
fix \( P \)
assume \( P\in \{P\in \text{Covers}(X).\ \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A\} \)
then have \( P\in \text{Covers}(X) \) and \( \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A \)
then obtain \( U \) where \( U\in \Phi \) and \( \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A \)
with assms, \( P\in \text{Covers}(X) \) have \( P \in (\bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \)
with \( U\in \Phi \) have \( P\in (\bigcup U\in \Phi .\ \bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \)
}
then show \( \{P\in \text{Covers}(X).\ \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A\} \subseteq \) \( (\bigcup U\in \Phi .\ \bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \) using subset_iff
{
fix \( P \)
assume \( P\in (\bigcup U\in \Phi .\ \bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \)
then obtain \( U \) where \( U\in \Phi \), \( P \in (\bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \)
with assms have \( P\in \text{Covers}(X) \) and \( \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A \)
with \( U\in \Phi \) have \( P\in \{P\in \text{Covers}(X).\ \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A\} \)
}
then show \( (\bigcup U\in \Phi .\ \bigcap x\in X.\ \{P\in \text{Covers}(X).\ \exists A\in P.\ U(\{x\}) \subseteq A\}) \subseteq \) \( \{P\in \text{Covers}(X).\ \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A\} \)
qed
then show \( thesis \) unfolding UniCovFromUniformity_def
qed

If \(\Phi\) is a (diagonal) uniformity on \(X\), then covers of the form \(\{ W\{ x\} : x\in X\}\) are members of \( \text{UniCovFromUniformity}(X,\Phi ) \).

lemma cover_image:

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

shows \( \{W\{x\}.\ x\in X\} \in \text{UniCovFromUniformity}(X,\Phi ) \)proof
let \( P = \{W\{x\}.\ x\in X\} \)
have \( P \in \text{Covers}(X) \)proof
from assms have \( W \subseteq X\times X \) and \( P \in Pow(Pow(X)) \) using entourage_props(1)
moreover
have \( \bigcup P = X \)proof
from \( W \subseteq X\times X \) show \( \bigcup P \subseteq X \)
from assms show \( X \subseteq \bigcup P \) using neigh_not_empty(2)
qed
ultimately show \( thesis \) unfolding Covers_def
qed
moreover
from assms(2) have \( \exists W\in \Phi .\ \forall x\in X.\ \exists A\in P.\ W\{x\} \subseteq A \)
ultimately show \( thesis \) unfolding UniCovFromUniformity_def
qed

If \(\Phi\) is a (diagonal) uniformity on \(X\), then every two elements of \( \text{UniCovFromUniformity}(X,\Phi ) \) have a common barycentric refinement.

lemma common_bar_refinemnt:

assumes \( \Phi \text{ is a uniformity on } X \), \( \Theta = \text{UniCovFromUniformity}(X,\Phi ) \), \( \mathcal{C} \in \Theta \), \( \mathcal{D} \in \Theta \)

shows \( \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^B \mathcal{C} ) \wedge (\mathcal{R} \lt ^B \mathcal{D} ) \)proof
from assms(2,3) obtain \( U \) where \( U\in \Phi \) and I: \( \forall x\in X.\ \exists C\in \mathcal{C} .\ U\{x\} \subseteq C \) unfolding UniCovFromUniformity_def
from assms(2,4) obtain \( V \) where \( V\in \Phi \) and II: \( \forall x\in X.\ \exists D\in \mathcal{D} .\ V\{x\} \subseteq D \) unfolding UniCovFromUniformity_def
from assms(1), \( U\in \Phi \), \( V\in \Phi \) have \( U\cap V \in \Phi \) unfolding IsUniformity_def, IsFilter_def
with assms(1) obtain \( W \) where \( W\in \Phi \) and \( W\circ W \subseteq U\cap V \) and \( W=converse(W) \) using half_size_symm
from assms(1), \( W\in \Phi \) have \( domain(W) \subseteq X \) unfolding IsUniformity_def, IsFilter_def
let \( P = \{W\{t\}.\ t\in X\} \)
have \( P\in \Theta \), \( P \lt ^B \mathcal{C} \), \( P \lt ^B \mathcal{D} \)proof
from assms(1,2), \( W\in \Phi \) show \( P\in \Theta \) using cover_image
with assms(2) have \( \bigcup P = X \) unfolding UniCovFromUniformity_def, Covers_def
{
fix \( x \)
assume \( x\in X \)
from \( W=converse(W) \), \( domain(W) \subseteq X \), \( W\circ W \subseteq U\cap V \) have \( \text{Star}(\{x\},P) \subseteq U\{x\} \) and \( \text{Star}(\{x\},P) \subseteq V\{x\} \) using rel_sq_image
from \( x\in X \), I obtain \( C \) where \( C\in \mathcal{C} \) and \( U\{x\} \subseteq C \)
with \( \text{Star}(\{x\},P) \subseteq U\{x\} \), \( C\in \mathcal{C} \) have \( \exists C\in \mathcal{C} .\ \text{Star}(\{x\},P) \subseteq C \)
moreover
from \( x\in X \), II obtain \( D \) where \( D\in \mathcal{D} \) and \( V\{x\} \subseteq D \)
with \( \text{Star}(\{x\},P) \subseteq V\{x\} \), \( D\in \mathcal{D} \) have \( \exists D\in \mathcal{D} .\ \text{Star}(\{x\},P) \subseteq D \)
ultimately have \( \exists C\in \mathcal{C} .\ \text{Star}(\{x\},P) \subseteq C \) and \( \exists D\in \mathcal{D} .\ \text{Star}(\{x\},P) \subseteq D \)
}
hence \( \forall x\in X.\ \exists C\in \mathcal{C} .\ \text{Star}(\{x\},P) \subseteq C \) and \( \forall x\in X.\ \exists D\in \mathcal{D} .\ \text{Star}(\{x\},P) \subseteq D \)
with \( \bigcup P = X \) show \( P \lt ^B \mathcal{C} \) and \( P \lt ^B \mathcal{D} \) unfolding IsBarycentricRefinement_def
qed
thus \( thesis \)
qed

If \(\Phi\) is a (diagonal) uniformity on \(X\), then every element of \( \text{UniCovFromUniformity}(X,\Phi ) \) has a barycentric refinement there.

corollary bar_refinement_ex:

assumes \( \Phi \text{ is a uniformity on } X \), \( \Theta = \text{UniCovFromUniformity}(X,\Phi ) \), \( \mathcal{C} \in \Theta \)

shows \( \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^B \mathcal{C} ) \) using assms, common_bar_refinemnt

If \(\Phi\) is a (diagonal) uniformity on \(X\), then \( \text{UniCovFromUniformity}(X,\Phi ) \) is a family of uniform covers.

theorem unicov_from_uniformity:

assumes \( \Phi \text{ is a uniformity on } X \) and \( X\neq 0 \)

shows \( \text{UniCovFromUniformity}(X,\Phi ) \text{ are uniform covers of } X \)proof
let \( \Theta = \text{UniCovFromUniformity}(X,\Phi ) \)
from assms(1) have \( \Theta \subseteq \text{Covers}(X) \) unfolding UniCovFromUniformity_def
moreover
from assms(1) have \( \{X\} \in \Theta \) unfolding Covers_def, IsUniformity_def, IsFilter_def, UniCovFromUniformity_def
hence \( \Theta \neq 0 \)
moreover
have \( \forall \mathcal{R} \in \Theta .\ \forall \mathcal{C} \in \text{Covers}(X).\ ((\mathcal{R} \lt ^* \mathcal{C} ) \longrightarrow \mathcal{C} \in \Theta ) \)proof
{
fix \( \mathcal{R} \) \( \mathcal{C} \)
assume \( \mathcal{R} \in \Theta \), \( \mathcal{C} \in \text{Covers}(X) \), \( \mathcal{R} \lt ^* \mathcal{C} \)
have \( \mathcal{C} \in \Theta \)proof
from \( \mathcal{R} \in \Theta \) obtain \( U \) where \( U\in \Phi \) and I: \( \forall x\in X.\ \exists R\in \mathcal{R} .\ U(\{x\}) \subseteq R \) unfolding UniCovFromUniformity_def
{
fix \( x \)
assume \( x\in X \)
with I obtain \( R \) where \( R\in \mathcal{R} \) and \( U(\{x\}) \subseteq R \)
from \( R\in \mathcal{R} \), \( \mathcal{R} \lt ^* \mathcal{C} \) obtain \( C \) where \( C\in \mathcal{C} \) and \( \text{Star}(R,\mathcal{R} ) \subseteq C \) unfolding IsStarRefinement_def
with \( U(\{x\}) \subseteq R \), \( R\in \mathcal{R} \) have \( U(\{x\}) \subseteq C \) using element_subset_star
with \( C\in \mathcal{C} \) have \( \exists C\in \mathcal{C} .\ U(\{x\}) \subseteq C \)
}
hence \( \forall x\in X.\ \exists C\in \mathcal{C} .\ U(\{x\}) \subseteq C \)
with \( U\in \Phi \), \( \mathcal{C} \in \text{Covers}(X) \) show \( thesis \) unfolding UniCovFromUniformity_def
qed
}
thus \( thesis \)
qed
moreover
have \( \forall \mathcal{C} \in \Theta .\ \forall \mathcal{D} \in \Theta .\ \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^* \mathcal{C} ) \wedge (\mathcal{R} \lt ^* \mathcal{D} ) \)proof
{
fix \( \mathcal{C} \) \( \mathcal{D} \)
assume \( \mathcal{C} \in \Theta \), \( \mathcal{D} \in \Theta \)
with assms(1) obtain \( P \) where \( P\in \Theta \) and \( P \lt ^B \mathcal{C} \), \( P \lt ^B \mathcal{D} \) using common_bar_refinemnt
from assms(1), \( P\in \Theta \) obtain \( \mathcal{R} \) where \( \mathcal{R} \in \Theta \) and \( \mathcal{R} \lt ^B P \) using bar_refinement_ex
from \( \mathcal{R} \in \Theta \), \( P\in \Theta \), \( \mathcal{C} \in \Theta \), \( \mathcal{D} \in \Theta \) have \( P \in \text{Covers}(X) \), \( \mathcal{R} \in \text{Covers}(X) \), \( \mathcal{C} \in \text{Covers}(X) \), \( \mathcal{D} \in \text{Covers}(X) \) unfolding UniCovFromUniformity_def
with assms(2), \( \mathcal{R} \lt ^B P \), \( P \lt ^B \mathcal{C} \), \( P \lt ^B \mathcal{D} \) have \( \mathcal{R} \lt ^* \mathcal{C} \) and \( \mathcal{R} \lt ^* \mathcal{D} \) using bary_bary_star
with \( \mathcal{R} \in \Theta \) have \( \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^* \mathcal{C} ) \wedge (\mathcal{R} \lt ^* \mathcal{D} ) \)
}
thus \( thesis \)
qed
ultimately show \( thesis \) unfolding AreUniformCovers_def
qed

The UniCovFromUniformity operation is the inverse of UniformityFromUniCov.

theorem unicov_from_unif_inv:

assumes \( \Theta \text{ are uniform covers of } X \), \( X\neq 0 \)

shows \( \text{UniCovFromUniformity}(X, \text{UniformityFromUniCov}(X,\Theta )) = \Theta \)proof
let \( \Phi = \text{UniformityFromUniCov}(X,\Theta ) \)
let \( L = \text{UniCovFromUniformity}(X,\Phi ) \)
from assms have I: \( \Phi \text{ is a uniformity on } X \) using uniformity_from_unicov
with assms(2) have II: \( L \text{ are uniform covers of } X \) using unicov_from_uniformity
{
fix \( P \)
assume \( P\in L \)
with I obtain \( Q \) where \( Q\in L \) and \( Q \lt ^B P \) using bar_refinement_ex
from \( Q\in L \) obtain \( U \) where \( U\in \Phi \) and III: \( \forall x\in X.\ \exists A\in Q.\ U\{x\} \subseteq A \) unfolding UniCovFromUniformity_def
from \( U\in \Phi \) have \( U \in \text{Supersets}(X\times X,\{\bigcup \{U\times U.\ U\in P\}.\ P\in \Theta \}) \) unfolding UniformityFromUniCov_def
then obtain \( B \) where \( B\subseteq X\times X \), \( B\subseteq U \) and \( \exists C\in \{\bigcup \{U\times U.\ U\in P\}.\ P\in \Theta \}.\ C\subseteq B \) unfolding Supersets_def
then obtain \( C \) where \( C \in \{\bigcup \{U\times U.\ U\in P\}.\ P\in \Theta \} \) and \( C\subseteq B \)
then obtain \( R \) where \( R\in \Theta \) and \( C = \bigcup \{V\times V.\ V\in R\} \)
with \( C\subseteq B \), \( B\subseteq U \) have \( \bigcup \{V\times V.\ V\in R\} \subseteq U \)
from assms(1), II, \( P\in L \), \( Q\in L \), \( R\in \Theta \) have IV: \( P\in \text{Covers}(X) \), \( Q\in \text{Covers}(X) \), \( R\in \text{Covers}(X) \) unfolding AreUniformCovers_def
have \( R \lt ^B Q \)proof
{
fix \( x \)
assume \( x\in X \)
with III obtain \( A \) where \( A\in Q \) and \( U\{x\} \subseteq A \)
with \( \bigcup \{V\times V.\ V\in R\} \subseteq U \) have \( (\bigcup \{V\times V.\ V\in R\})\{x\} \subseteq A \)
with \( A\in Q \) have \( \exists A\in Q.\ \text{Star}(\{x\},R) \subseteq A \) using star_singleton
}
then have \( \forall x\in X.\ \exists A\in Q.\ \text{Star}(\{x\},R) \subseteq A \)
moreover
from \( R\in \text{Covers}(X) \) have \( \bigcup R = X \) unfolding Covers_def
ultimately show \( thesis \) unfolding IsBarycentricRefinement_def
qed
with assms(2), \( Q \lt ^B P \), IV have \( R \lt ^* P \) using bary_bary_star
with assms(1), \( R\in \Theta \), \( P\in \text{Covers}(X) \) have \( P\in \Theta \) unfolding AreUniformCovers_def
}
thus \( L\subseteq \Theta \)
{
fix \( P \)
assume \( P\in \Theta \)
with assms(1) have \( P \in \text{Covers}(X) \) unfolding AreUniformCovers_def
from assms(1), \( P\in \Theta \) obtain \( Q \) where \( Q \in \Theta \) and \( Q \lt ^B P \) using unicov_has_bar_ref
let \( A = \bigcup \{V\times V.\ V\in Q\} \)
have \( A \in \Phi \)proof
from assms(1), \( Q\in \Theta \) have \( A \subseteq X\times X \) and \( A \in \{\bigcup \{V\times V.\ V\in Q\}.\ Q\in \Theta \} \) unfolding AreUniformCovers_def, Covers_def
then show \( thesis \) using superset_gen unfolding UniformityFromUniCov_def
qed
with I obtain \( B \) where \( B\in \Phi \), \( B\circ B \subseteq A \) and \( B=converse(B) \) using half_size_symm
let \( R = \{B\{x\}.\ x\in X\} \)
from I, II, \( B\in \Phi \) have \( R\in L \) and \( \bigcup R =X \) using cover_image unfolding UniCovFromUniformity_def, Covers_def
have \( R \lt ^B P \)proof
{
fix \( x \)
assume \( x\in X \)
from assms(1), \( Q \in \Theta \) have \( \bigcup Q = X \) unfolding AreUniformCovers_def, Covers_def
with \( Q \lt ^B P \), \( x\in X \) obtain \( C \) where \( C\in P \) and \( \text{Star}(\{x\},Q) \subseteq C \) unfolding IsBarycentricRefinement_def
from \( B=converse(B) \), I, \( B\in \Phi \) have \( \text{Star}(\{x\},R) = (B\circ B)\{x\} \) using uni_domain, rel_sq_image
moreover
from \( (B\circ B) \subseteq A \) have \( (B\circ B)\{x\} \subseteq A\{x\} \)
moreover
have \( A\{x\} = \text{Star}(\{x\},Q) \) using star_singleton
ultimately have \( \text{Star}(\{x\},R) \subseteq \text{Star}(\{x\},Q) \)
with \( \text{Star}(\{x\},Q) \subseteq C \), \( C\in P \) have \( \exists C\in P.\ \text{Star}(\{x\},R) \subseteq C \)
}
with \( \bigcup R = X \) show \( thesis \) unfolding IsBarycentricRefinement_def
qed
with assms(2), II, \( P \in \text{Covers}(X) \), \( R\in L \), \( R \lt ^B P \) have \( P\in L \) using unicov_bary_cov
}
thus \( \Theta \subseteq L \)
qed

The UniformityFromUniCov operation is the inverse of UniCovFromUniformity.

theorem unif_from_unicov_inv:

assumes \( \Phi \text{ is a uniformity on } X \), \( X\neq 0 \)

shows \( \text{UniformityFromUniCov}(X, \text{UniCovFromUniformity}(X,\Phi )) = \Phi \)proof
let \( \Theta = \text{UniCovFromUniformity}(X,\Phi ) \)
let \( L = \text{UniformityFromUniCov}(X,\Theta ) \)
from assms have I: \( \Theta \text{ are uniform covers of } X \) using unicov_from_uniformity
with assms have II: \( L \text{ is a uniformity on } X \) using uniformity_from_unicov
{
fix \( A \)
assume \( A\in \Phi \)
with assms(1) obtain \( B \) where \( B\in \Phi \), \( B\circ B \subseteq A \) and \( B = converse(B) \) using half_size_symm
from assms(1), \( A\in \Phi \) have \( A \subseteq X\times X \) using uni_domain(1)
let \( P = \{B\{x\}.\ x\in X\} \)
from assms(1), \( B\in \Phi \) have \( P\in \Theta \) using cover_image
let \( C = \bigcup \{U\times U.\ U\in P\} \)
from I, \( P\in \Theta \) have \( C\in L \) unfolding AreUniformCovers_def using basic_unif
from assms(1), \( B\in \Phi \), \( B = converse(B) \), \( B\circ B \subseteq A \) have \( C \subseteq A \) using uni_domain(2), symm_sq_prod_image
with II, \( A \subseteq X\times X \), \( C\in L \) have \( A\in L \) unfolding IsUniformity_def, IsFilter_def
}
thus \( \Phi \subseteq L \)
{
fix \( A \)
assume \( A\in L \)
with II have \( A \subseteq X\times X \) using entourage_props(1)
from \( A\in L \) obtain \( P \) where \( P\in \Theta \) and \( \bigcup \{U\times U.\ U\in P\} \subseteq A \) unfolding UniformityFromUniCov_def, Supersets_def
from \( P\in \Theta \) obtain \( B \) where \( B\in \Phi \) and III: \( \forall x\in X.\ \exists V\in P.\ B\{x\} \subseteq V \) unfolding UniCovFromUniformity_def
have \( B\subseteq A \)proof
from assms(1), \( B\in \Phi \) have \( B \subseteq \bigcup \{B\{x\}\times B\{x\}.\ x\in X\} \) using entourage_props(1,2), refl_union_singl_image
moreover
have \( \bigcup \{B\{x\}\times B\{x\}.\ x\in X\} \subseteq A \)proof
{
fix \( x \)
assume \( x\in X \)
with III obtain \( V \) where \( V\in P \) and \( B\{x\} \subseteq V \)
hence \( B\{x\}\times B\{x\} \subseteq \bigcup \{U\times U.\ U\in P\} \)
}
hence \( \bigcup \{B\{x\}\times B\{x\}.\ x\in X\} \subseteq \bigcup \{U\times U.\ U\in P\} \)
with \( \bigcup \{U\times U.\ U\in P\} \subseteq A \) show \( thesis \)
qed
ultimately show \( thesis \)
qed
with assms(1), \( B\in \Phi \), \( A \subseteq X\times X \) have \( A\in \Phi \) unfolding IsUniformity_def, IsFilter_def
}
thus \( L\subseteq \Phi \)
qed
end
Definition of Covers: \( \text{Covers}(X) \equiv \{P \in Pow(Pow(X)).\ \bigcup P = X\} \)
Definition of Star: \( \text{Star}(R,\mathcal{R} ) \equiv \bigcup \{S\in \mathcal{R} .\ S\cap R \neq 0\} \)
lemma star_mono:

assumes \( U\subseteq V \)

shows \( \text{Star}(U,P) \subseteq \text{Star}(V,P) \)
Definition of IsBarycentricRefinement: \( P \lt ^B Q \equiv \forall x\in \bigcup P.\ \exists U\in Q.\ \text{Star}(\{x\},P) \subseteq U \)
Definition of IsStarRefinement: \( P \lt ^* Q \equiv \forall U\in P.\ \exists V\in Q.\ \text{Star}(U,P) \subseteq V \)
corollary star_single_mono:

assumes \( x\in U \)

shows \( \text{Star}(\{x\},P) \subseteq \text{Star}(U,P) \)
lemma cover_nonempty:

assumes \( X\neq 0 \), \( P \in \text{Covers}(X) \)

shows \( \exists U\in P.\ U\neq 0 \)
Definition of AreUniformCovers: \( \Theta \text{ are uniform covers of } X \equiv \Theta \subseteq \text{Covers}(X) \wedge \Theta \neq 0 \wedge \) \( (\forall \mathcal{R} \in \Theta .\ \forall \mathcal{C} \in \text{Covers}(X).\ ((\mathcal{R} \lt ^* \mathcal{C} ) \longrightarrow \mathcal{C} \in \Theta )) \wedge \) \( (\forall \mathcal{C} \in \Theta .\ \forall \mathcal{D} \in \Theta .\ \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^* \mathcal{C} ) \wedge (\mathcal{R} \lt ^* \mathcal{D} )) \)
lemma cover_stref_triv:

assumes \( P \in \text{Covers}(X) \)

shows \( P \lt ^* \{X\} \)
lemma unicov_contains_triv:

assumes \( \Theta \text{ are uniform covers of } X \)

shows \( \{X\} \in \Theta \)
lemma unicov_has_star_ref:

assumes \( \Theta \text{ are uniform covers of } X \) and \( P\in \Theta \)

shows \( \exists Q\in \Theta .\ (Q \lt ^* P) \)
lemma star_is_bary:

assumes \( Q\in \text{Covers}(X) \) and \( Q \lt ^* P \)

shows \( Q \lt ^B P \)
corollary unicov_has_bar_ref:

assumes \( \Theta \text{ are uniform covers of } X \) and \( P\in \Theta \)

shows \( \exists Q\in \Theta .\ (Q \lt ^B P) \)
lemma bary_bary_star:

assumes \( P\in \text{Covers}(X) \), \( Q\in \text{Covers}(X) \), \( R\in \text{Covers}(X) \), \( P \lt ^B Q \), \( Q \lt ^B R \), \( X\neq 0 \)

shows \( P \lt ^* R \)
lemma rel_compdef: shows \( \langle x,z\rangle \in r\circ s \longleftrightarrow (\exists y.\ \langle x,y\rangle \in s \wedge \langle y,z\rangle \in r) \)
Definition of UniformityFromUniCov: \( \text{UniformityFromUniCov}(X,\Theta ) \equiv \text{Supersets}(X\times X,\{\bigcup \{U\times U.\ U\in P\}.\ P\in \Theta \}) \)
Definition of Supersets: \( \text{Supersets}(X,\mathcal{A} ) \equiv \{B\in Pow(X).\ \exists A\in \mathcal{A} .\ A\subseteq B\} \)
lemma star_ref_mem:

assumes \( U\in P \), \( P \lt ^*Q \) and \( \bigcup \{W\times W.\ W\in Q\} \subseteq A \)

shows \( U\times U \subseteq A \)
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 rel_square_starr: shows \( (\bigcup \{U\times U.\ U\in P\})\circ (\bigcup \{U\times U.\ U\in P\}) = \bigcup \{U\times \text{Star}(U,P).\ U\in P\} \)
lemma element_subset_star:

assumes \( U\in P \)

shows \( U \subseteq \text{Star}(U,P) \)
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 UniCovFromUniformity: \( \text{UniCovFromUniformity}(X,\Phi ) \equiv \{P\in \text{Covers}(X).\ \exists U\in \Phi .\ \forall x\in X.\ \exists A\in P.\ U(\{x\}) \subseteq A\} \)
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 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 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 cover_image:

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

shows \( \{W\{x\}.\ x\in X\} \in \text{UniCovFromUniformity}(X,\Phi ) \)
lemma rel_sq_image:

assumes \( W = converse(W) \), \( domain(W) \subseteq X \)

shows \( \text{Star}(\{x\},\{W\{t\}.\ t\in X\}) = (W\circ W)\{x\} \)
lemma common_bar_refinemnt:

assumes \( \Phi \text{ is a uniformity on } X \), \( \Theta = \text{UniCovFromUniformity}(X,\Phi ) \), \( \mathcal{C} \in \Theta \), \( \mathcal{D} \in \Theta \)

shows \( \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^B \mathcal{C} ) \wedge (\mathcal{R} \lt ^B \mathcal{D} ) \)
corollary bar_refinement_ex:

assumes \( \Phi \text{ is a uniformity on } X \), \( \Theta = \text{UniCovFromUniformity}(X,\Phi ) \), \( \mathcal{C} \in \Theta \)

shows \( \exists \mathcal{R} \in \Theta .\ (\mathcal{R} \lt ^B \mathcal{C} ) \)
theorem uniformity_from_unicov:

assumes \( \Theta \text{ are uniform covers of } X \), \( X\neq 0 \)

shows \( \text{UniformityFromUniCov}(X,\Theta ) \text{ is a uniformity on } X \)
theorem unicov_from_uniformity:

assumes \( \Phi \text{ is a uniformity on } X \) and \( X\neq 0 \)

shows \( \text{UniCovFromUniformity}(X,\Phi ) \text{ are uniform covers of } X \)
lemma star_singleton: shows \( (\bigcup \{V\times V.\ V\in P\})\{x\} = \text{Star}(\{x\},P) \)
lemma superset_gen:

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

shows \( A \in \text{Supersets}(X,\mathcal{A} ) \)
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 unicov_bary_cov:

assumes \( \Theta \text{ are uniform covers of } X \), \( P\in \Theta \), \( Q \in \text{Covers}(X) \), \( P \lt ^B Q \) and \( X\neq 0 \)

shows \( Q\in \Theta \)
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 basic_unif:

assumes \( \Theta \subseteq \text{Covers}(X) \), \( P\in \Theta \)

shows \( \bigcup \{U\times U.\ U\in P\} \in \text{UniformityFromUniCov}(X,\Theta ) \)
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 symm_sq_prod_image:

assumes \( converse(r) = r \)

shows \( r\circ r = \bigcup \{(r\{x\})\times (r\{x\}).\ x \in domain(r)\} \)
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 refl_union_singl_image:

assumes \( A \subseteq X\times X \) and \( id(X)\subseteq A \)

shows \( A \subseteq \bigcup \{A\{x\}\times A\{x\}.\ x \in X\} \)