IsarMathLib

In the MetricSpace_ZF we show how a single (ordered loop valued) pseudometric defines a uniformity. In this theory we extend this to the situation where we have an arbitrary collection of pseudometrics, all defined on the the same set \(X\) and valued in an ordered loop \(L\). Since real numbers form an ordered loop all results proven in this theory are true for the standard real-valued pseudometrics.

Suppose \(\mathcal{M}\) is a collection of (an ordered loop valued) pseudometrics on \(X\), i.e. \(d:X\times X\rightarrow L^+\) is a pseudometric for every \(d\in \mathcal{M}\). Then, for each \(d\in \mathcal{M}\) the collection of sets \(\mathfrak{B} = \{ d^{-1}(\{c\in L^+: c\leq b\}): b \in L_+ \}\) forms a fundamental system of entourages. Consequently, by taking supersets of \(\mathfrak{B}\) we can get a uniformity defined by the pseudometric (see theorem metric_gauge_base in the MetricSpace_ZF theory. Repeating this process for each \(d\in \mathcal{M}\) we obtain a collection of uniformities on \(X\). Since all uniformities on \(X\) ordered by inclusion form a complete lattice (see theorem uniformities_compl_latt in the UniformityLattice_ZF) there exists the smallest (coarsest) uniformity that contains all uniformities defined by the pseudometrics in \(\mathcal{M}\).

To shorten the main definition let's define the uniformity derived from a single pseudometric as UnifFromPseudometric. In the definition below \(X\) is the underlying set, \(L,A,r\) are the carrier, binary operation and the order relation, resp., of the ordered loop where the pseudometrics takes its values and \(d\) is the pseudometrics.

We construct the uniformity from a collection of pseudometrics \(\mathcal{M}\) by taking the supremumum (i.e. the least upper upper bound) of the collection of uniformities defined by each pseudometric from \(\mathcal{M}\).

The context muliple_pmetric is very similar to the pmetric_space context except that rather than fixing a single pseudometric \(d\) we fix a nonempty collection of pseudometrics \(\mathcal{M}\). That forces the notation for disk, topology, interior and closure to depend on the pseudometric \(d\). The \(\mathcal{U}\) symbol will denote the collection of uniformities generated by \(\mathcal{M}\). We also assume that the positive cone \(L_+\) of the loop is nonempty, \(r\) down-directs \(L_+\) (see Order_ZF for definition) and that the (positive cone of the) ordered loop is halfable (see \( MetricSpace\_ZF) \)). In short, we assume what we need for ordered loop valued pseudometrics to generate uniformities.

If \(d\) is one of the pseudometrics from \(\mathcal{M}\) then theorems proven in the pmetric_space context are valid as applied to \(d\).

In the muliple_pmetric context each element of \(\mathcal{U}\) is a uniformity.

The uniformity generated by a family of pseudometrics \(\mathcal{M}\) is indeed a uniformity which is the supremum of uniformities in \(\mathcal{U}\).

The uniformity generated by a family of pseudometrics contains all uniformities generated by the pseudometrics in \(\mathcal{M}\).

If a uniformity contains all uniformities generated by the pseudometrics in \(\mathcal{M}\) then it contains the uniformity generated by that family of pseudometrics.

The uniformity generated by the collection of pseudometrics \(\mathcal{M}\) contains all inverse images of the initial segments of the positive cone of \(L\), (i.e. sets of the form \(d^{-1}(\{c\in l: 0 \leq c \leq y \})\) for \(d\in \mathcal{M}\) and \(y\) from the positive cone \(L_+\) of \(L\)).

The uniformity generated by the collection of pseudometrics \(\mathcal{M}\) is the coarsest uniformity that contains all inverse images of the initial segments of the positive cone of \(L\) with respect to all \(d\in\mathcal{M}\).

This section presents an alternative, more direct approach to defining a uniformity generated by a collection of pseudometric. This approach is probably equivalent to the one presented in the previous section, but more complicated and hence obsolete.

The next two definitions describe the way a common fundamental system of entourages for \(\mathcal{M}\) is constructed. First we take finite subset \(M\) of \(\mathcal{M}\). Then we choose \(f:M\rightarrow L_+\). This way for each \(d\in M\) the value \(f(d)\) is a positive element of \(L\) and \(\{d^{-1}(\{c\in L^+: c\leq f(d)\}): d\in M\}\) is a finite collection of subsets of \(X\times X\). Then we take intersections of such finite collections as \(M\) varies over \(\mathcal{M}\) and \(f\) varies over all possible functions mapping \(M\) to \(L_+\). To simplify notation for this construction we split it into two steps. In the first step we define a collection of finite intersections resulting from choosing a finite set of pseudometrics \(M\), \(f:M\rightarrow L_+\) and varying the selector function \(f\) over the space of functions mapping \(M\) to the set of positive elements of \(L\).

In the second step we collect all uniform gauge sets defined above as parameter \(M\) vary over all nonempty finite subsets of \(\mathcal{M}\). This is the collection of sets that we will show forms a fundamental system of entourages.

Analogously what is done in the pmetric_space context we will write \( \text{UniformGauges}(X,L,A,r,\mathcal{M} ) \) as \( \mathfrak{B} \) in the muliple_pmetric context.

The next lemma just shows the definition of \(\mathfrak{B}\) in notation used in the muliple_pmetric.

\(\mathfrak{B}\) consists of (finite) intersections of sets of the form \(d^{-1}(\{c\in L^+:c\leq f(d)\})\) where \(f:M\rightarrow L_+\) some finite subset \(M\subseteq \mathcal{M}\). More precisely, if \(M\) is a nonempty finite subset of \(\mathcal{M}\) and \(f\) maps \(M\) to the positive set of the loop \(L\), then the set \(\bigcap_{d\in M} d^{-1}(\{c\in L^+:c\leq f(d)\}\) is in \(\mathfrak{B}\).

If \(d\) is member of any finite subset of \(\mathcal{M}\) then \(d\) maps \(X\times X\) to the nonnegative set of the ordered loop \(L\).

Members of the uniform gauge defined by multiple pseudometrics are subsets of \(X\times X\) i.e. relations on \(X\).

Suppose \(M_1\) is a subset of \(M\) and \(\mathcal{M}\). \(f_1,f\) map \(M_1\) and \(M\), resp. to \(L_+\) and \(f\leq f_1\) on \(M_1\). Then the set \(\bigcap_{d\in M} d^{-1}(\{y \in L_+: y\leq f(d)\})\) is included in the set \(\bigcap_{d\in M_1} d^{-1}(\{y \in L_+: y\leq f_1(d)\})\).

For any two sets \(B_1,B_2\) in \(\mathfrak{B}\) there exist a third one that is contained in both.

Sets in \(\mathfrak{B}\) contain the diagonal and are symmetric, hence contain a symmetric subset from \(\mathfrak{B}\).

\(\mathfrak{B}\) is a subset of the power set of \(X\times X\).

If \(\mathcal{M}\) and \(L_+\) are nonempty then \(\mathfrak{B}\) is also nonempty.

If the loop order is halfable then for every set \(B_1\in \mathfrak{B}\) there is another set \(B_2\in \mathfrak{B}\) such that \(B_2\circ B_2 \subseteq B_1\).

If \(\mathcal{M}\) is a nonempty collection of pseudometrics on a nonempty set \(X\) valued in loop \(L\) partially ordered by relation \(r\) such that the set of positive elements \(L_+\) is nonempty, \(r\) down directs \(L_+\) and \(r\) is halfable on \(L\),then \(\mathfrak{B}\) is a fundamental system of entourages in \(X\) hence its supersets form a uniformity on \(X\) and hence those supersets define a topology on \(X\)

The notion of uniformity can be defined in several ways. Our primary definition in the UniformSpace_ZF theory is based on the concept of entourages. In UniformSpace_ZF_2 we consider the an alternative definition based on uniform covers. The third possible definition is based on families of pseudometrics. "The significance of defining a uniformity by means of a family of pseudometrics lies in the fact that all unifomities can be so obtained." (from Bourbaki: General Topology Chapter IX par. 1.4). In this section we formalize a part of the material that is needed to prove this statement that can be done without the Axiom of Choice and in the general setting of ordered-loop valued pseudometrics.

The definition of a uniformity requires that for each entourage \(U\) there is another one \(V\) such that \(V\circ V\subseteq U\). Furthermore, lemma half_size_symm shows that we can assume \(V\) is symmetric. In some propositions in this section we will assume that we are given a function say \(h\) that provides those half-size entourages, i.e. maps a uniformity \(\Phi\) into itself and for each entourage \(U\in\Phi\) we have \(h(U)\circ h(U)\subseteq V\).

The existence of such function follows from the Axiom of Choice, but we don't want to use AC in this theory.

The next definition lists the desired properties of such halving function for shorter references in theorem assumptions.

Let \(\Phi\) be a uniformity on \(X\), \(U\in\Phi\) and \(h\) is a halving function for \(\Phi\). This function then defines inductively a sequence \(\{ H_n\}_{n\in\mathbb{N}}\) of entourages such that \(H_0 = U\) and \(H_{n+1}\circ H_{n+1}\subseteq H_n\). The next lemma shows that \(H\) is a \(\Phi\)-valued sequence which starts at \(U\).

For the inductively defined sequence of halving entourages \(H\) starting from \(U\) and a natural number \(n\) we indeed have \(H_{n+1} \circ H_{n+1} \subseteq H_n\).

A halving sequence in \(\Phi\) is decreasing in the inclusion order on \(\Phi\), hence the inclusion order on \(\Phi\) is total on the sequence's image of the natural numbers, hence total on the sequence's image of positive natural numbers. We need that fact about positive natural numbers because we plan to prove that the image of the sequence on the positive natural numbers forms a fundamental system of symmetric entourages. and the first element of the sequence (at index \(0\)) does not have to be symmetric.

We aim at showing that the a halving sequence image is a uniform base. The next lemma shows the first condition in the uniform base definition: for two sets in a halving sequence image there is a third one that is contained in both.

Sets in the halving sequence image of positive naturals contain the diagonal, are symmetric and for every such set \(B\) there is another one contained in the converse of the first one and another one \(B_2\) such that \(B_2\circ B_2\subseteq B_1\). Note the symmetry of the sets is not required in the definition of a fundamental system of entourages, but it's good to have as we plan to construct a pseudometric that generates that halving sequence image of positive naturals.

The halving sequence image of positive naturals is contained in the powerset of \(X\times X\) and is not empty.

If \(\Phi\) is a uniformity, \(h\) is a halving function for it and \(U\in \Phi\) then the image of the halving sequence defined inductively as \(H_0=U, H_{n+1} = h(H(n))\) on the positive naturals is a fundamental system of entourages.

Theorem halving_seq_base shows that given a halving function \(h\) for a uniformity \(\Phi\) each entourage \(U\in\Phi\) defines a uniformity that has a countable base consisting of symmetric entourages and (as we show later) contains that entourage. The next definition summarizes the construction of this coarser uniformity.

If \(\Phi\) is a uniformity, \(h\) is a halving function for it and \(U\in\Phi\) then \( \text{CountBaseUnif}(X,h,U) \) is a uniformity on \(X\) that contains \(U\) (as a member) and is contained in \(\Phi\).

If \(\Phi\) is a uniformity on a nonempty set \(X\) and admits a halving function \(h\) then \(\Phi\) is the supremum of the collection of uniformities \(\{\Psi_U: U\in\Phi\}\) in the inclusion order relation, where \(\Psi_U = \)\( \text{CountBaseUnif}(X,h,U) \). Since \(\Psi_U\) has a countable base this shows that every uniformity (that admits a halving function) is a union and a supremum of some collection of uniformities each of which has a countable base.