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: