# 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 \{A \in Pow(Pow(X)).\ \bigcup A = X\}$$

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 $$R\in \mathcal{R}$$

shows $$R \subseteq \text{Star}(R,\mathcal{R} )$$ using assms unfolding Star_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

$$\mathcal{R} \lt ^* \mathcal{C} \equiv \forall R\in \mathcal{R} .\ \exists C\in \mathcal{C} .\ \text{Star}(R,\mathcal{R} ) \subseteq C$$

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

lemma cover_stref_triv:

assumes $$\mathcal{C} \in \text{Covers}(X)$$

shows $$\mathcal{C} \lt ^* \{X\}$$ using assms unfolding Star_def , IsStarRefinement_def , Covers_def

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

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

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 unform covers.

Definition

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

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

theorem uniformity_from_unicov:

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

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(2), $$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(2), $$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(2), $$P\in \Theta$$ have $$\bigcup \{U\times U.\ U\in P\} \in \Phi$$ unfolding AreUniformCovers_def , Covers_def , UniformityFromUniCov_def , Supersets_def
from assms(2), $$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(2), $$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 assms(2), $$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
end
Definition of Star: $$\text{Star}(R,\mathcal{R} ) \equiv \bigcup \{S\in \mathcal{R} .\ S\cap R \neq 0\}$$
Definition of IsStarRefinement: $$\mathcal{R} \lt ^* \mathcal{C} \equiv \forall R\in \mathcal{R} .\ \exists C\in \mathcal{C} .\ \text{Star}(R,\mathcal{R} ) \subseteq C$$
Definition of Covers: $$\text{Covers}(X) \equiv \{A \in Pow(Pow(X)).\ \bigcup A = X\}$$
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 $$\mathcal{C} \in \text{Covers}(X)$$

shows $$\mathcal{C} \lt ^* \{X\}$$
lemma unicov_contains_triv:

assumes $$\Theta \text{ are uniform covers of } X$$

shows $$\{X\} \in \Theta$$
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 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 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 $$R\in \mathcal{R}$$

shows $$R \subseteq \text{Star}(R,\mathcal{R} )$$
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 )$$
65
60
19
19