# 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 an alternative definition based of the notion of uniform covers.

### 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. The members of such family are 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}(U,P) \equiv \bigcup \{V\in P.\ V\cap U \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 unif_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 unif_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 unif_props , 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}(U,P) \equiv \bigcup \{V\in P.\ V\cap U \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 unif_props:

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

shows $$A \subseteq X\times X$$ and $$id(X) \subseteq A$$
lemma neigh_not_empty:

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

shows $$V\{x\} \neq 0$$ and $$x \in V\{x\}$$
lemma half_size_symm:

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

shows $$\exists W\in \Phi .\ W\circ W \subseteq U \wedge W=converse(W)$$
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 unif_props:

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

shows $$A \subseteq X\times X$$ and $$id(X) \subseteq A$$
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\}$$
268
172
63
63