IsarMathLib

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

theory UniformityLattice_ZF imports Cardinal_ZF Order_ZF_1a UniformSpace_ZF

begin

In this theory we consider the collection of all uniformities on a arbitrary set \(X\). Since unformities are sets of subsets of \(X\times X\) such set of uniformities is naturally ordered by the inclusion relation. Specifically, for two uniformities \(\mathcal{U}_1\) and \(\mathcal{U}_2\) on a set \(X\) if \(\mathcal{U}_1 \subseteq \mathcal{U}_2\) we say that \(\mathcal{U}_2\) is finer than \(\mathcal{U}_1\) or that \(\mathcal{U}_1\) is coarser than \(\mathcal{U}_2\). In this theory we show that with this order the collection of uniformities forms a complete lattice.

Uniformities on a fixed set as a partially ordered set

In this section we introduce the definitions of the set of uniformities on \(X\) and show that the inclusion relation is on this set makes it a partially ordered set (a poset) with a maximum and minimum.

We define \( \text{Uniformities}(X) \) as the set of all uniformities on \(X\).

definition

\( \text{Uniformities}(X) \equiv \{\Phi \in Pow(Pow(X\times X)).\ \Phi \text{ is a uniformity on } X\} \)

If \(\Phi\) is a uniformity on \(X\), then \(\Phi\) is a collection of subsets of \(X\times X\), hence it's a member of \( \text{Uniformities}(X) \).

lemma unif_in_unifs:

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

shows \( \Phi \in \text{Uniformities}(X) \) using assms unfolding Uniformities_def, IsUniformity_def, IsFilter_def

For nonempty sets the set of uniformities is not empty as well.

lemma unifomities_exist:

assumes \( X\neq \emptyset \)

shows \( \text{Uniformities}(X)\neq \emptyset \) unfolding Uniformities_def using assms, min_uniformity

Uniformities on a set \(X\) are naturally ordered by inclusion, we call the resulting order relation OrderOnUniformities.

definition

\( \text{OrderOnUniformities}(X) \equiv \text{InclusionOn}( \text{Uniformities}(X)) \)

For the order on uniformities two uniformities are in relation iff one is contained in the other.

lemma order_unif_iff:

assumes \( \Phi \in \text{Uniformities}(X) \), \( \Psi \in \text{Uniformities}(X) \)

shows \( \langle \Phi ,\Psi \rangle \in \text{OrderOnUniformities}(X) \longleftrightarrow \Phi \subseteq \Psi \) using assms unfolding OrderOnUniformities_def, InclusionOn_def

The order defined by inclusion on uniformities is a partial order.

lemma ord_unif_partial_ord:

shows \( \text{IsPartOrder}( \text{Uniformities}(X), \text{OrderOnUniformities}(X)) \) unfolding OrderOnUniformities_def using incl_is_partorder

In particular, the order defined by inclusion on uniformities is antisymmetric. Having this as a separate fact is handy as we reference some lemmas proven for antisymmetric (not necessarily partial order) relations.

lemma ord_unif_antisymm:

shows \( \text{antisym}( \text{OrderOnUniformities}(X)) \) using ord_unif_partial_ord unfolding IsPartOrder_def

If \(X\) is not empty then the singleton \(\{ X\times X\}\) is the minimal element of the set of uniformities on \(X\) ordered by inclusion and the collection of subsets of \(X\times X\) that contain the diagonal is the maximal element.

theorem uniformities_min_max:

assumes \( X\neq \emptyset \)

shows \( \text{HasAminimum}( \text{OrderOnUniformities}(X), \text{Uniformities}(X)) \), \( \text{Minimum}( \text{OrderOnUniformities}(X), \text{Uniformities}(X)) = \{X\times X\} \), \( \text{HasAmaximum}( \text{OrderOnUniformities}(X), \text{Uniformities}(X)) \), \( \text{Maximum}( \text{OrderOnUniformities}(X), \text{Uniformities}(X)) = \{U\in Pow(X\times X).\ id(X)\subseteq U\} \)proof

let \( \mathfrak{U} = \text{Uniformities}(X) \)

let \( r = \text{OrderOnUniformities}(X) \)

let \( M = \{U\in Pow(X\times X).\ id(X)\subseteq U\} \)

from assms have \( \{X\times X\} \in \mathfrak{U} \) and \( M\in \mathfrak{U} \) unfolding Uniformities_def using min_uniformity, max_uniformity

{

fix \( \Phi \)

assume \( \Phi \in \mathfrak{U} \)

with \( \{X\times X\}\in \mathfrak{U} \) have \( \langle \{X\times X\},\Phi \rangle \in r \) unfolding Uniformities_def, OrderOnUniformities_def, InclusionOn_def using min_uniformity1

}

with \( \{X\times X\} \in \mathfrak{U} \) show \( \text{HasAminimum}(r,\mathfrak{U} ) \) and \( \text{Minimum}(r,\mathfrak{U} ) = \{X\times X\} \) unfolding HasAminimum_def using Order_ZF_4_L15, ord_unif_antisymm

{

fix \( \Phi \)

assume \( \Phi \in \mathfrak{U} \)

then have \( \Phi \subseteq M \) unfolding IsUniformity_def, Uniformities_def

with \( M\in \mathfrak{U} \), \( \Phi \in \mathfrak{U} \) have \( \langle \Phi ,M\rangle \in r \) unfolding OrderOnUniformities_def, InclusionOn_def

}

with \( M\in \mathfrak{U} \) show \( \text{HasAmaximum}(r,\mathfrak{U} ) \) and \( \text{Maximum}(r,\mathfrak{U} ) = M \) unfolding HasAmaximum_def using Order_ZF_4_L14, ord_unif_antisymm

qed

Least upper bound of a set of uniformities

In this section we show that inclusion order on the collection of unformities on a fixed set is (Dedekind) complete i.e. every nonempty set of uniformities has a least upper bound.

Given a set of uniformities \(\mathcal{U}\) on \(X\) we define a collection of subsets of \(X\) called LUB_UnifBase (the least upper bound base in comments) as the set of all products of nonempty finite subsets of \(\bigcup\mathcal{U}\). The "least upper bound base" term is not justified at this point, but we will show later that this set is actually a uniform base (i.e. a fundamental system of entourages) on \(X\) and hence the supersets of it form a uniformity on \(X\), which is the supremum (i.e. the least upper bound) of \(\mathcal{U}\).

definition

\( \text{LUB_UnifBase}(\mathcal{U} ) = \{\bigcap M.\ M \in \text{FinPow}(\bigcup \mathcal{U} )\setminus \{\emptyset \}\} \)

For any two sets in the least upper bound base there is a third one contained in both.

lemma lub_unif_base_1st_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U_1 \in \text{LUB_UnifBase}(\mathcal{U} ) \), \( U_2 \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( \exists U_3\in \text{LUB_UnifBase}(\mathcal{U} ).\ U_3\subseteq U_1\cap U_2 \)proof

let \( \mathcal{F} = \text{FinPow}(\bigcup \mathcal{U} )\setminus \{\emptyset \} \)

from assms(2,3) obtain \( M_1 \) \( M_2 \) where \( M_1\in \mathcal{F} \), \( M_1\neq \emptyset \), \( U_1=\bigcap M_1 \), \( M_2\in \mathcal{F} \), \( M_2\neq \emptyset \), \( U_2=\bigcap M_2 \) unfolding LUB_UnifBase_def

let \( M_3 = M_1\cup M_2 \)

from \( M_1\neq \emptyset \), \( M_2\neq \emptyset \), \( U_1=\bigcap M_1 \), \( U_2=\bigcap M_2 \) have \( \bigcap M_3 \subseteq U_1\cap U_2 \)

with \( M_1 \in \mathcal{F} \), \( M_2 \in \mathcal{F} \), \( U_2=\bigcap M_2 \) show \( thesis \) using union_finpow unfolding LUB_UnifBase_def

qed

Each set in the least upper bound base contains the diagonal of \(X\times X\).

lemma lub_unif_base_2nd_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( id(X)\subseteq U \) using assms unfolding LUB_UnifBase_def, FinPow_def, Uniformities_def, IsUniformity_def

The converse of each set from the least upper bound base contains a set from it.

lemma lub_unif_base_3rd_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U_1 \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( \exists U_2 \in \text{LUB_UnifBase}(\mathcal{U} ).\ U_2 \subseteq converse(U_1) \)proof

let \( \mathcal{F} = \text{FinPow}(\bigcup \mathcal{U} )\setminus \{\emptyset \} \)

from assms(2) obtain \( M_1 \) where \( M_1\in \mathcal{F} \), \( M_1\neq \emptyset \), \( U_1=\bigcap M_1 \) unfolding LUB_UnifBase_def

let \( M_2 = \{converse(V).\ V\in M_1\} \)

from assms(1), \( M_1\in \mathcal{F} \) have \( \forall V\in M_1.\ converse(V) \in \bigcup \mathcal{U} \) unfolding FinPow_def, Uniformities_def using entourage_props(4)

with \( M_1\in \mathcal{F} \) have \( \bigcap M_2 \in \text{LUB_UnifBase}(\mathcal{U} ) \) using fin_image_fin0 unfolding LUB_UnifBase_def

from assms(1), \( M_1\in \mathcal{F} \), \( U_1=\bigcap M_1 \) have \( \bigcap M_2 \subseteq converse(U_1) \) unfolding Uniformities_def, FinPow_def using prod_converse

with \( \bigcap M_2 \in \text{LUB_UnifBase}(\mathcal{U} ) \) show \( thesis \)

qed

For each set (relation) \(U_1\) from the least upper bound base there is another one \(U_2\) such that \(U_2\) composed with itself is contained in \(U_1\).

lemma lub_unif_base_4th_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U_1 \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( \exists U_2 \in \text{LUB_UnifBase}(\mathcal{U} ).\ U_2\circ U_2 \subseteq U_1 \)proof

let \( \mathcal{F} = \text{FinPow}(\bigcup \mathcal{U} )\setminus \{\emptyset \} \)

from assms(2) obtain \( M_1 \) where \( M_1\in \mathcal{F} \), \( M_1\neq \emptyset \), \( U_1=\bigcap M_1 \) unfolding LUB_UnifBase_def

from \( M_1\in \mathcal{F} \) have \( Finite(M_1) \) unfolding FinPow_def

{

fix \( V \)

assume \( V\in M_1 \)

with assms(1), \( M_1\in \mathcal{F} \) obtain \( \Phi \) where \( \Phi \in \mathcal{U} \) and \( V\in \Phi \) unfolding FinPow_def

with assms(1), \( V\in \Phi \) obtain \( W \) where \( W\in \Phi \) and \( W\circ W \subseteq V \) unfolding Uniformities_def using entourage_props(3)

with \( \Phi \in \mathcal{U} \) have \( \exists W\in \bigcup \mathcal{U} .\ W\circ W \subseteq V \)

}

hence \( \forall V\in M_1.\ \exists W\in \bigcup \mathcal{U} .\ W\circ W \subseteq V \)

with \( Finite(M_1) \) have \( \exists f\in M_1\rightarrow \bigcup \mathcal{U} .\ \forall V\in M_1.\ f(V)\circ f(V) \subseteq V \) by (rule finite_choice_fun )

then obtain \( f \) where \( f:M_1\rightarrow \bigcup \mathcal{U} \) and \( \forall V\in M_1.\ f(V)\circ f(V) \subseteq V \)

let \( M_2 = \{f(V).\ V\in M_1\} \)

from \( f:M_1\rightarrow \bigcup \mathcal{U} \) have \( \forall V\in M_1.\ f(V) \in \bigcup \mathcal{U} \) using apply_funtype

with \( M_1\in \mathcal{F} \) have \( \bigcap M_2 \in \text{LUB_UnifBase}(\mathcal{U} ) \) using fin_image_fin0 unfolding LUB_UnifBase_def

from \( M_1\neq \emptyset \), \( \forall V\in M_1.\ f(V)\circ f(V) \subseteq V \) have \( (\bigcap V\in M_1.\ f(V))\circ (\bigcap V\in M_1.\ f(V)) \subseteq (\bigcap V\in M_1.\ V) \) by (rule square_incl_product )

with \( U_1=\bigcap M_1 \), \( \bigcap M_2 \in \text{LUB_UnifBase}(\mathcal{U} ) \) show \( thesis \)

qed

The least upper bound base is a collection of relations on \(X\).

lemma lub_unif_base_5th_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \)

shows \( \text{LUB_UnifBase}(\mathcal{U} ) \subseteq Pow(X\times X) \) using assms unfolding Uniformities_def, FinPow_def, LUB_UnifBase_def

If a collection of uniformities is nonempty, then the least upper bound base is non-empty as well.

lemma lub_unif_base_6th_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( \text{LUB_UnifBase}(\mathcal{U} ) \neq \emptyset \)proof

from assms(2) obtain \( \Phi \) where \( \Phi \in \mathcal{U} \)

with assms(1) have \( \bigcup \mathcal{U} \neq \emptyset \) unfolding Uniformities_def using uniformity_non_empty

then show \( \text{LUB_UnifBase}(\mathcal{U} ) \neq \emptyset \) using finpow_nempty_nempty unfolding LUB_UnifBase_def

qed

If a collection of uniformities \(\mathcal{U}\) is nonempty, \(\mathcal{B}\) denotes the least upper bound base for \(\mathcal{U}\), then \(\mathcal{B}\) is a uniform base on \(X\), hence its supersets form a uniformity on \(X\) and the uniform topology generated by that uniformity is indeed a topology on \(X\).

theorem lub_unif_base_base:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

defines \( \mathfrak{B} \equiv \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( \mathfrak{B} \text{ is a uniform base on } X \), \( \text{Supersets}(X\times X,\mathfrak{B} ) \text{ is a uniformity on } X \), \( \text{UniformTopology}( \text{Supersets}(X\times X,\mathfrak{B} ),X) \text{ is a topology } \), \( \bigcup \text{UniformTopology}( \text{Supersets}(X\times X,\mathfrak{B} ),X) = X \) using assms, lub_unif_base_1st_cond, lub_unif_base_2nd_cond, lub_unif_base_3rd_cond, lub_unif_base_4th_cond, lub_unif_base_5th_cond, lub_unif_base_6th_cond, uniformity_base_is_base, uniform_top_is_top unfolding IsUniformityBaseOn_def

At this point we know that supersets with respect to \(X\times X\) of the least upper bound base for a collection of uniformities \(\mathcal{U}\) form a uniformity. To shorten the notation we will call this uniformity \( \text{LUB_Unif}(X,\mathcal{U} ) \).

definition

\( \text{LUB_Unif}(X,\mathcal{U} ) \equiv \text{Supersets}(X\times X,\text{LUB_UnifBase}(\mathcal{U} )) \)

With this definition we can rewrite some asssertions of theorem lub_unif_base_base in bit shorter form:

corollary lub_unif_base_base1:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( \text{LUB_Unif}(X,\mathcal{U} ) \text{ is a uniformity on } X \), \( \text{UniformTopology}(\text{LUB_Unif}(X,\mathcal{U} ),X) \text{ is a topology } \), \( \bigcup \text{UniformTopology}(\text{LUB_Unif}(X,\mathcal{U} ),X) = X \) using assms, lub_unif_base_base unfolding LUB_Unif_def

For any collection of uniformities \(\mathcal{U}\) on a nonempty set \(X\) the \( \text{LUB_Unif}(X,\mathcal{U} ) \) collection defined above is indeed an upper bound of \(\mathcal{U}\) in the order defined by the inclusion relation.

lemma lub_unif_upper_bound:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \Phi \in \mathcal{U} \)

shows \( \langle \Phi ,\text{LUB_Unif}(X,\mathcal{U} )\rangle \in \text{OrderOnUniformities}(X) \)proof

let \( \Psi = \text{LUB_Unif}(X,\mathcal{U} ) \)

from assms have \( \Psi \in \text{Uniformities}(X) \) unfolding LUB_Unif_def using lub_unif_base_base(2), unif_in_unifs

from assms(2,3) have \( \Phi \in \text{Uniformities}(X) \) and \( \Phi \text{ is a uniformity on } X \) unfolding Uniformities_def

{

fix \( E \)

assume \( E\in \Phi \)

with assms(3) have \( E \in \text{LUB_UnifBase}(\mathcal{U} ) \) using singleton_in_finpow unfolding LUB_UnifBase_def

with \( \Phi \text{ is a uniformity on } X \), \( E\in \Phi \) have \( E \in \Psi \) using entourage_props(1), superset_gen unfolding LUB_Unif_def

}

hence \( \Phi \subseteq \Psi \)

with \( \Phi \in \text{Uniformities}(X) \), \( \Psi \in \text{Uniformities}(X) \) show \( thesis \) unfolding OrderOnUniformities_def, InclusionOn_def

qed

Any upper bound (in the order defined by inclusion relation) of a nonempty collection of uniformities \(\mathcal{U}\) on a nonempty set \(X\) is greater or equal (in that order) than \( \text{LUB_Unif}(X,\mathcal{U} ) \). Together with lub_unif_upper_bound it means that \( \text{LUB_Unif}(X,\mathcal{U} ) \) is indeed the least upper bound of \(\mathcal{U}\).

lemma lub_unif_lub:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \) and \( \forall \Phi \in \mathcal{U} .\ \langle \Phi ,\Psi \rangle \in \text{OrderOnUniformities}(X) \)

shows \( \langle \text{LUB_Unif}(X,\mathcal{U} ),\Psi \rangle \in \text{OrderOnUniformities}(X) \)proof

from assms(3,4) have \( \Psi \in \text{Uniformities}(X) \) unfolding OrderOnUniformities_def, InclusionOn_def

then have \( \Psi \text{ is a filter on } (X\times X) \) unfolding Uniformities_def, IsUniformity_def

from assms(4) have \( \text{FinPow}(\bigcup \mathcal{U} )\setminus \{\emptyset \} \subseteq \text{FinPow}(\Psi )\setminus \{\emptyset \} \) unfolding OrderOnUniformities_def, InclusionOn_def, FinPow_def

with \( \Psi \text{ is a filter on } (X\times X) \) have \( \text{LUB_UnifBase}(\mathcal{U} ) \subseteq \Psi \) using filter_fin_inter_closed unfolding LUB_UnifBase_def

with \( \Psi \text{ is a filter on } (X\times X) \) have \( \text{LUB_Unif}(X,\mathcal{U} ) \subseteq \Psi \) using filter_superset_closed unfolding LUB_Unif_def

with assms(1,2,3), \( \Psi \in \text{Uniformities}(X) \) show \( thesis \) using lub_unif_base_base(2), unif_in_unifs unfolding LUB_Unif_def, OrderOnUniformities_def, InclusionOn_def

qed

A nonempty collection \(\mathcal{U}\) of uniformities on \(X\) has a supremum (i.e. the least upper bound) which is a uniformity.

theorem lub_unif_sup:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( \text{HasAsupremum}( \text{OrderOnUniformities}(X),\mathcal{U} ) \), \( \text{LUB_Unif}(X,\mathcal{U} ) = \text{Supremum}( \text{OrderOnUniformities}(X),\mathcal{U} ) \), \( \text{Supremum}( \text{OrderOnUniformities}(X),\mathcal{U} ) \text{ is a uniformity on } X \)proof

let \( r = \text{OrderOnUniformities}(X) \)

let \( S = \text{LUB_Unif}(X,\mathcal{U} ) \)

from assms(1,2) have \( \text{antisym}(r) \) and \( \forall \Phi \in \mathcal{U} .\ \langle \Phi ,S\rangle \in r \) using ord_unif_antisymm, lub_unif_upper_bound

from assms have I: \( \forall \Psi .\ (\forall \Phi \in \mathcal{U} .\ \langle \Phi ,\Psi \rangle \in r) \longrightarrow \langle S,\Psi \rangle \in r \) using lub_unif_lub

with assms(3), \( \text{antisym}(r) \), \( \forall \Phi \in \mathcal{U} .\ \langle \Phi ,S\rangle \in r \) show \( \text{HasAsupremum}(r,\mathcal{U} ) \) unfolding HasAsupremum_def using Order_ZF_5_L5(1)

from assms(3), \( \text{antisym}(r) \), \( \forall \Phi \in \mathcal{U} .\ \langle \Phi ,S\rangle \in r \), I show \( S = \text{Supremum}(r,\mathcal{U} ) \) using Order_ZF_5_L5(2)

from assms have \( S \text{ is a uniformity on } X \) using lub_unif_base_base1(1)

with \( S = \text{Supremum}(r,\mathcal{U} ) \) show \( \text{Supremum}(r,\mathcal{U} ) \text{ is a uniformity on } X \)

qed

The order on uniformities derived from inclusion is complete.

theorem uniformities_complete:

assumes \( X\neq \emptyset \)

shows \( \text{OrderOnUniformities}(X) \text{ is complete } \)proof

let \( r = \text{OrderOnUniformities}(X) \)

{

fix \( \mathcal{U} \)

assume \( \mathcal{U} \neq \emptyset \) and \( \text{IsBoundedAbove}(\mathcal{U} ,r) \)

then obtain \( \Psi \) where \( \forall \Phi \in \mathcal{U} .\ \langle \Phi ,\Psi \rangle \in r \) unfolding IsBoundedAbove_def

then have \( \mathcal{U} \subseteq \text{Uniformities}(X) \) unfolding OrderOnUniformities_def, InclusionOn_def

with assms, \( \mathcal{U} \neq \emptyset \) have \( \text{HasAsupremum}(r,\mathcal{U} ) \) using lub_unif_sup

}

then show \( r \text{ is complete } \) unfolding HasAsupremum_def, IsComplete_def

qed

Greatest lower bound of a set of uniformities

In this this section we show that every set of uniformities on fixed set \(X\) has an greatest lower bound, i.e. an infimum. The approach taken in the previous section to show the existence of the lowest upper bound of a collection of uniformities does not work for the greatest lower bound. The collection defined as the set of all products of nonempty finite subsets of \(\bigcap\mathcal{U}\) in general is not a fundamental system of entourages. Even though the first three conditions hold for such collection, the fourth one does not. The approach that works is to show the the supremum of the collection of lower bounds is actually a lower bound, hence the maximum of the set of lower bounds.

To shorten the proofs we introduce the concept of the supremum of the the collection of lower bounds of some collection of uniformities \(\mathcal{U}\). We know from the previous section that such supremum exists. Later in this section we show that this supremum is itself a lower bound of \(\mathcal{U}\), so it's the greatest lower bound i.e. infimum of \(\mathcal{U}\).

definition

\( SLB\_Unif(X,\mathcal{U} ) \equiv \text{Supremum}( \text{OrderOnUniformities}(X),\{\Psi \in \text{Uniformities}(X).\ \Psi \subseteq \bigcap \mathcal{U} \}) \)

The set of lower bounds of a nonempty set of uniformities is nonempty.

lemma lb_nempty_nempty:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( \{\Psi \in \text{Uniformities}(X).\ \Psi \subseteq \bigcap \mathcal{U} \} \neq \emptyset \)proof

from assms have \( \{X\times X\} \in \text{Uniformities}(X) \) and \( (X\times X) \in \bigcap \mathcal{U} \) using min_uniformity, min_uniformity1 unfolding Uniformities_def

thus \( thesis \)

qed

The supremum of the set of lower bounds of a collection of uniformities is a lower bound of that collection.

lemma unif_slb_is_lb:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( SLB\_Unif(X,\mathcal{U} ) \subseteq \bigcap \mathcal{U} \)proof

fix \( E \)

assume \( E\in SLB\_Unif(X,\mathcal{U} ) \)

let \( \mathcal{L} = \{\Psi \in \text{Uniformities}(X).\ \Psi \subseteq \bigcap \mathcal{U} \} \)

let \( \Xi = \text{LUB_Unif}(X,\mathcal{L} ) \)

let \( \mathfrak{B} = \text{LUB_UnifBase}(\mathcal{L} ) \)

have \( \mathcal{L} \subseteq \text{Uniformities}(X) \)

from assms, \( \mathcal{L} \subseteq \text{Uniformities}(X) \), \( E\in SLB\_Unif(X,\mathcal{U} ) \) have \( \Xi \text{ is a uniformity on } X \) and \( E\in \Xi \) using lub_unif_sup, lub_unif_base_base(2), lb_nempty_nempty unfolding LUB_Unif_def, SLB_Unif_def

with assms(1), \( \mathcal{L} \subseteq \text{Uniformities}(X) \), \( E\in SLB\_Unif(X,\mathcal{U} ) \) have \( \Xi \text{ is a uniformity on } X \) and \( E\in \Xi \) using lub_unif_sup, lub_unif_base_base(2) unfolding LUB_Unif_def, SLB_Unif_def

then have \( E\subseteq X\times X \) using entourage_props(1)

from \( E\in \Xi \) obtain \( B \) where \( B\subseteq X\times X \), \( B\in \mathfrak{B} \), \( B\subseteq E \) unfolding LUB_Unif_def, Supersets_def

from \( B\in \mathfrak{B} \) obtain \( M \) where \( M\in \text{FinPow}(\bigcup \mathcal{L} ) \), \( M\neq \emptyset \) and \( B=\bigcap M \) unfolding LUB_UnifBase_def

from \( M\in \text{FinPow}(\bigcup \mathcal{L} ) \) have \( M \subseteq \bigcap \mathcal{U} \) unfolding FinPow_def

{

fix \( \Phi \)

assume \( \Phi \in \mathcal{U} \)

with \( M \subseteq \bigcap \mathcal{U} \), \( \Phi \in \mathcal{U} \), \( M\in \text{FinPow}(\bigcup \mathcal{L} ) \) have \( M\in \text{FinPow}(\Phi ) \) unfolding FinPow_def

from assms(2), \( \Phi \in \mathcal{U} \) have \( \Phi \text{ is a filter on } (X\times X) \) unfolding Uniformities_def using unif_filter

with \( M\in \text{FinPow}(\Phi ) \), \( M\neq \emptyset \), \( B=\bigcap M \) have \( B\in \Phi \) using filter_fin_inter_closed

with \( E\subseteq X\times X \), \( B\subseteq E \), \( \Phi \text{ is a filter on } (X\times X) \) have \( E\in \Phi \) unfolding IsFilter_def

}

with assms(3) show \( E\in \bigcap \mathcal{U} \)

qed

Let \(\mathfrak{U}\) denote the collection of all uniformities on a nonempty set \(X\), ordered by inclusion. Then every collection of uniformities \(\mathcal{U}\subseteq \mathfrak{U}\) has an infimum (the greatest lower bound) which is equal to the supremum of the collection of lower bounds.

theorem unif_inf:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( \text{HasAnInfimum}( \text{OrderOnUniformities}(X),\mathcal{U} ) \) and \( \text{Infimum}( \text{OrderOnUniformities}(X),\mathcal{U} ) = SLB\_Unif(X,\mathcal{U} ) \)proof

let \( r = \text{OrderOnUniformities}(X) \)

let \( \mathcal{L} = \{\Psi \in \text{Uniformities}(X).\ \Psi \subseteq \bigcap \mathcal{U} \} \)

from assms have \( \mathcal{L} \subseteq \text{Uniformities}(X) \) and \( \mathcal{L} \neq \emptyset \) using lb_nempty_nempty

with assms have \( \text{HasAmaximum}(r,\mathcal{L} ) \) and \( \text{Maximum}(r,\mathcal{L} ) = \text{Supremum}(r,\mathcal{L} ) \) using lub_unif_sup, lub_unif_sup(3), unif_in_unifs, unif_slb_is_lb, ord_unif_antisymm, sup_is_max unfolding SLB_Unif_def

have \( (\bigcap \Phi \in \mathcal{U} .\ r^{-1}\{\Phi \}) = \mathcal{L} \)proof

have \( r \subseteq \text{Uniformities}(X)\times \text{Uniformities}(X) \) unfolding OrderOnUniformities_def, InclusionOn_def

with assms(3) have \( (\bigcap \Phi \in \mathcal{U} .\ r^{-1}\{\Phi \}) = \{\Psi \in \text{Uniformities}(X).\ \forall \Phi \in \mathcal{U} .\ \langle \Psi ,\Phi \rangle \in r\} \) using lower_bounds

also

from assms(2,3) have \( .\ .\ .\ = \mathcal{L} \) using order_unif_iff

finally show \( thesis \)

qed

with \( \text{HasAmaximum}(r,\mathcal{L} ) \) show \( \text{HasAnInfimum}( \text{OrderOnUniformities}(X),\mathcal{U} ) \) unfolding HasAnInfimum_def

from \( (\bigcap \Phi \in \mathcal{U} .\ r^{-1}\{\Phi \}) = \mathcal{L} \), \( \text{Maximum}(r,\mathcal{L} ) = \text{Supremum}(r,\mathcal{L} ) \) show \( \text{Infimum}(r,\mathcal{U} ) = SLB\_Unif(X,\mathcal{U} ) \) unfolding Infimum_def, SLB_Unif_def

qed

end

Definition of Uniformities: \( \text{Uniformities}(X) \equiv \{\Phi \in Pow(Pow(X\times X)).\ \Phi \text{ is a uniformity on } X\} \)

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 IsFilter: \( \mathfrak{F} \text{ is a filter on } X \equiv (\emptyset \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 min_uniformity:

assumes \( X\neq \emptyset \)

shows \( \{X\times X\} \text{ is a uniformity on } X \)

Definition of OrderOnUniformities: \( \text{OrderOnUniformities}(X) \equiv \text{InclusionOn}( \text{Uniformities}(X)) \)

Definition of InclusionOn: \( \text{InclusionOn}(X) \equiv \{p\in X\times X.\ \text{fst}(p) \subseteq \text{snd}(p)\} \)

lemma incl_is_partorder: shows \( \text{IsPartOrder}(X, \text{InclusionOn}(X)) \)

lemma ord_unif_partial_ord: shows \( \text{IsPartOrder}( \text{Uniformities}(X), \text{OrderOnUniformities}(X)) \)

Definition of IsPartOrder: \( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)

lemma max_uniformity:

assumes \( X\neq \emptyset \)

shows \( \{U\in Pow(X\times X).\ id(X)\subseteq U\} \text{ is a uniformity on } X \)

lemma min_uniformity1:

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

shows \( (X\times X) \in \Phi \)

Definition of HasAminimum: \( \text{HasAminimum}(r,A) \equiv \exists m\in A.\ \forall x\in A.\ \langle m,x\rangle \in r \)

lemma Order_ZF_4_L15:

assumes \( \text{antisym}(r) \) and \( m \in A \) and \( \forall a\in A.\ \langle m,a\rangle \in r \)

shows \( \text{Minimum}(r,A) = m \)

lemma ord_unif_antisymm: shows \( \text{antisym}( \text{OrderOnUniformities}(X)) \)

Definition of HasAmaximum: \( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)

lemma Order_ZF_4_L14:

assumes \( \text{antisym}(r) \) and \( M \in A \) and \( \forall a\in A.\ \langle a,M\rangle \in r \)

shows \( \text{Maximum}(r,A) = M \)

Definition of LUB_UnifBase: \( \text{LUB_UnifBase}(\mathcal{U} ) = \{\bigcap M.\ M \in \text{FinPow}(\bigcup \mathcal{U} )\setminus \{\emptyset \}\} \)

lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \)

Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(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 fin_image_fin0:

assumes \( N \in \text{FinPow}(B)\setminus \{\emptyset \} \) and \( \forall V\in N.\ K(V)\in C \)

shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C)\setminus \{\emptyset \} \)

lemma prod_converse:

assumes \( M \subseteq Pow(X\times X) \)

shows \( \bigcap \{converse(A).\ A\in M\} = converse(\bigcap M) \)

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 finite_choice_fun:

assumes \( Finite(X) \), \( \forall x\in X.\ \exists y\in Y.\ P(x,y) \)

shows \( \exists f\in X\rightarrow Y.\ \forall x\in X.\ P(x,f(x)) \)

lemma square_incl_product:

assumes \( I\neq \emptyset \), \( \forall i\in I.\ A(i)\circ A(i) \subseteq B(i) \)

shows \( (\bigcap i\in I.\ A(i))\circ (\bigcap i\in I.\ A(i)) \subseteq (\bigcap i\in I.\ B(i)) \)

lemma uniformity_non_empty:

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

shows \( \Phi \neq \emptyset \)

lemma finpow_nempty_nempty:

assumes \( X\neq \emptyset \)

shows \( \text{FinPow}(X)\setminus \{\emptyset \} \neq \emptyset \)

lemma lub_unif_base_1st_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U_1 \in \text{LUB_UnifBase}(\mathcal{U} ) \), \( U_2 \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( \exists U_3\in \text{LUB_UnifBase}(\mathcal{U} ).\ U_3\subseteq U_1\cap U_2 \)

lemma lub_unif_base_2nd_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( id(X)\subseteq U \)

lemma lub_unif_base_3rd_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U_1 \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( \exists U_2 \in \text{LUB_UnifBase}(\mathcal{U} ).\ U_2 \subseteq converse(U_1) \)

lemma lub_unif_base_4th_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( U_1 \in \text{LUB_UnifBase}(\mathcal{U} ) \)

shows \( \exists U_2 \in \text{LUB_UnifBase}(\mathcal{U} ).\ U_2\circ U_2 \subseteq U_1 \)

lemma lub_unif_base_5th_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \)

shows \( \text{LUB_UnifBase}(\mathcal{U} ) \subseteq Pow(X\times X) \)

lemma lub_unif_base_6th_cond:

assumes \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( \text{LUB_UnifBase}(\mathcal{U} ) \neq \emptyset \)

theorem uniformity_base_is_base:

assumes \( X\neq \emptyset \) and \( \mathfrak{B} \text{ is a uniform base on } X \)

shows \( \text{Supersets}(X\times X,\mathfrak{B} ) \text{ is a uniformity on } X \)

theorem uniform_top_is_top:

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

shows \( \text{UniformTopology}(\Phi ,X) \text{ is a topology } \) and \( \bigcup \text{UniformTopology}(\Phi ,X) = X \)

Definition of IsUniformityBaseOn: \( \mathfrak{B} \text{ is a uniform base on } X \equiv \) \( (\forall B_1\in \mathfrak{B} .\ \forall B_2\in \mathfrak{B} .\ \exists B_3\in \mathfrak{B} .\ B_3\subseteq B_1\cap B_2) \wedge (\forall B\in \mathfrak{B} .\ id(X)\subseteq B) \wedge \) \( (\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1)) \wedge (\forall B_1\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1) \wedge \) \( \mathfrak{B} \subseteq Pow(X\times X) \wedge \mathfrak{B} \neq \emptyset \)

theorem lub_unif_base_base:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

defines \( \mathfrak{B} \equiv \text{LUB_UnifBase}(\mathcal{U} ) \)

Definition of LUB_Unif: \( \text{LUB_Unif}(X,\mathcal{U} ) \equiv \text{Supersets}(X\times X,\text{LUB_UnifBase}(\mathcal{U} )) \)

theorem lub_unif_base_base:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

defines \( \mathfrak{B} \equiv \text{LUB_UnifBase}(\mathcal{U} ) \)

lemma unif_in_unifs:

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

shows \( \Phi \in \text{Uniformities}(X) \)

lemma singleton_in_finpow:

assumes \( x \in X \)

shows \( \{x\} \in \text{FinPow}(X) \)

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 superset_gen:

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

shows \( A \in \text{Supersets}(X,\mathcal{A} ) \)

lemma filter_fin_inter_closed:

assumes \( \mathfrak{F} \text{ is a filter on } X \), \( M\in \text{FinPow}(\mathfrak{F} )\setminus \{\emptyset \} \)

shows \( \bigcap M \in \mathfrak{F} \)

lemma filter_superset_closed:

assumes \( \mathfrak{F} \text{ is a filter on } X \), \( \mathcal{A} \subseteq \mathfrak{F} \)

shows \( \text{Supersets}(X,\mathcal{A} ) \subseteq \mathfrak{F} \)

lemma lub_unif_upper_bound:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \Phi \in \mathcal{U} \)

shows \( \langle \Phi ,\text{LUB_Unif}(X,\mathcal{U} )\rangle \in \text{OrderOnUniformities}(X) \)

lemma lub_unif_lub:

shows \( \langle \text{LUB_Unif}(X,\mathcal{U} ),\Psi \rangle \in \text{OrderOnUniformities}(X) \)

Definition of HasAsupremum: \( \text{HasAsupremum}(r,A) \equiv \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)

lemma Order_ZF_5_L5:

assumes \( \text{antisym}(r) \) and \( A\neq 0 \) and \( \forall x\in A.\ \langle x,z\rangle \in r \) and \( \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle z,y\rangle \in r \)

shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \)

lemma Order_ZF_5_L5:

shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \)

corollary lub_unif_base_base1:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

Definition of IsBoundedAbove: \( \text{IsBoundedAbove}(A,r) \equiv ( A=\emptyset \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)

theorem lub_unif_sup:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

Definition of IsComplete: \( r \text{ is complete } \equiv \) \( \forall A.\ \text{IsBoundedAbove}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)

lemma lb_nempty_nempty:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( \{\Psi \in \text{Uniformities}(X).\ \Psi \subseteq \bigcap \mathcal{U} \} \neq \emptyset \)

Definition of SLB_Unif: \( SLB\_Unif(X,\mathcal{U} ) \equiv \text{Supremum}( \text{OrderOnUniformities}(X),\{\Psi \in \text{Uniformities}(X).\ \Psi \subseteq \bigcap \mathcal{U} \}) \)

Definition of Supersets: \( \text{Supersets}(X,\mathcal{A} ) \equiv \{B\in Pow(X).\ \exists A\in \mathcal{A} .\ A\subseteq B\} \)

lemma unif_filter:

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

shows \( \Phi \text{ is a filter on } (X\times X) \)

theorem lub_unif_sup:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

lemma unif_slb_is_lb:

assumes \( X\neq \emptyset \), \( \mathcal{U} \subseteq \text{Uniformities}(X) \), \( \mathcal{U} \neq \emptyset \)

shows \( SLB\_Unif(X,\mathcal{U} ) \subseteq \bigcap \mathcal{U} \)

lemma sup_is_max:

assumes \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \), \( \text{Supremum}(r,A) \in A \)

shows \( \text{HasAmaximum}(r,A) \) and \( \text{Maximum}(r,A) = \text{Supremum}(r,A) \)