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