Note: this theory is a work in progress. The approach take is probably not the right one. The right approach is through the notion of least upper bound of a collection of uniformities.
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 sets \(\{ d^{-1}(\{c\in L^+: c\leq b\}): b \in L_+ \}\) form a fundamental system of entourages (see MetricSpace_ZF).
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\).
definition
\( \text{UniformGaugeSets}(X,L,A,r,M) \equiv \) \( \{(\bigcap d\in M.\ d^{-1}(\{c\in \text{Nonnegative}(L,A,r).\ \langle c,f(d)\rangle \in r\})).\ f\in M\rightarrow \text{PositiveSet}(L,A,r)\} \)
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.
definition
\( \text{UniformGauges}(X,L,A,r,\mathcal{M} ) \equiv \bigcup M\in \text{FinPow}(\mathcal{M} )\setminus \{\emptyset \}.\ \text{UniformGaugeSets}(X,L,A,r,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 collection of pseudometrics \(\mathcal{M}\). That forces the notation for disk, topology, interior and closure to depend on the pseudometric \(d\).
locale muliple_pmetric = loop1 +
assumes mpmetricAssm: \( \forall d\in \mathcal{M} .\ \text{IsApseudoMetric}(d,X,L,A,r) \)
defines \( disk(d,c,R) \equiv \text{Disk}(X,d,r,c,R) \)
defines \( \tau (d) \equiv \text{MetricTopology}(X,L,A,r,d) \)
defines \( int(d,D) \equiv \text{Interior}(D,\tau (d)) \)
defines \( cl(d,D) \equiv \text{Closure}(D,\tau (d)) \)
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.
abbreviation (in muliple_pmetric)
\( \mathfrak{B} \equiv \text{UniformGauges}(X,L,A,r,\mathcal{M} ) \)
The next lemma just shows the definition of \(\mathfrak{B}\) in notation used in the muliple_pmetric.
lemma (in muliple_pmetric) mgauge_def_alt:
shows \( \mathfrak{B} = (\bigcup M\in \text{FinPow}(\mathcal{M} )\setminus \{\emptyset \}.\ \{(\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})).\ f\in M\rightarrow L_+\}) \) unfolding UniformGaugeSets_def, UniformGauges_def\(\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}\).
lemma (in muliple_pmetric) mgauge_finset_fun:
assumes \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \), \( f:M\rightarrow L_+ \)
shows \( (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \in \mathfrak{B} \) using assms, mgauge_def_altIf \(d\) is one of the pseudometrics from \(\mathcal{M}\) then theorems proven in pmetric_space can are valid.
lemma (in muliple_pmetric) pmetric_space_valid_in_mpm:
assumes \( d\in \mathcal{M} \)
shows \( pmetric\_space(L,A,r,d,X) \)proofIf \(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\).
lemma (in muliple_pmetric) each_pmetric_map:
assumes \( M\in \text{FinPow}(\mathcal{M} ) \) and \( d\in M \)
shows \( d: X\times X \rightarrow L^+ \) using assms, pmetric_space_valid_in_mpm, pmetric_properties(1) unfolding FinPow_defMembers of the uniform gauge defined by multiple pseudometrics are subsets of \(X\times X\) i.e. relations on \(X\).
lemma (in muliple_pmetric) muniform_gauge_relations:
assumes \( B\in \mathfrak{B} \)
shows \( B\subseteq X\times X \)proofSuppose \(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)\})\).
lemma (in muliple_pmetric) fun_inter_vimage_mono:
assumes \( M_1\subseteq \mathcal{M} \), \( M_1\subseteq M \), \( M_1\neq \emptyset \), \( f_1:M_1\rightarrow L_+ \), \( f:M\rightarrow L_+ \) and \( \forall d\in M_1.\ f(d)\leq f_1(d) \)
shows \( (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \subseteq (\bigcap d\in M_1.\ d^{-1}(\{c\in L^+.\ c\leq f_1(d)\})) \)proofFor any two sets \(B_1,B_2\) in \(\mathfrak{B}\) there exist a third one that is contained in both.
lemma (in muliple_pmetric) mgauge_1st_cond:
assumes \( r \text{ down-directs } L_+ \), \( B_1\in \mathfrak{B} \), \( B_2\in \mathfrak{B} \)
shows \( \exists B\in \mathfrak{B} .\ B\subseteq B_1\cap B_2 \)proofSets in \(\mathfrak{B}\) contain the diagonal and are symmetric, hence contain a symmetric subset from \(\mathfrak{B}\).
lemma (in muliple_pmetric) mgauge_2nd_and_3rd_cond:
assumes \( B\in \mathfrak{B} \)
shows \( id(X)\subseteq B \), \( B = converse(B) \), \( \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B) \)proof\(\mathfrak{B}\) is a subset of the power set of \(X\times X\).
lemma (in muliple_pmetric) mgauge_5thCond:
shows \( \mathfrak{B} \subseteq Pow(X\times X) \) using muniform_gauge_relationsIf \(\mathcal{M}\) and \(L_+\) are nonempty then \(\mathfrak{B}\) is also nonempty.
lemma (in muliple_pmetric) mgauge_6thCond:
assumes \( \mathcal{M} \neq \emptyset \) and \( L_+\neq \emptyset \)
shows \( \mathfrak{B} \neq \emptyset \)proofIf 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\).
lemma (in muliple_pmetric) mgauge_4thCond:
assumes \( \text{IsHalfable}(L,A,r) \), \( B_1\in \mathfrak{B} \)
shows \( \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1 \)proofIf \(\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\)
lemma (in muliple_pmetric) mmetric_gauge_base:
assumes \( X\neq \emptyset \), \( \mathcal{M} \neq \emptyset \), \( L_+\neq \emptyset \), \( r \text{ down-directs } L_+ \), \( \text{IsHalfable}(L,A,r) \)
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, mgauge_1st_cond, mgauge_2nd_and_3rd_cond, mgauge_4thCond, mgauge_5thCond, mgauge_6thCond, uniformity_base_is_base, uniform_top_is_top unfolding IsUniformityBaseOn_defThe formula for defining the fundamental system of entourages from a collection of pseudometrics given in lemma mgauge_def_alt is a bit different than the standard one found in the literature on real-valued pseudometrics. In this section we explore another alternative to defining fundamental system of entourages common to a collection of pseudometrics.
Any pseudometrics \(d:X\times X\rightarrow L^+\) defines a fundamental system of entourages on \(X\) by the formula \(\mathcal{B}(d) = \{ d^{-1}(\{c\in L^+: c\leq b\}): b \in L_+ \}\) (see theorem metric_gauge_base in Metric_Space_ZF theory.
definition (in muliple_pmetric)
\( \mathcal{B} (d) \equiv \{d^{-1}(\{c\in L^+.\ c\leq b\}).\ b\in L_+\} \)
Every subset \(M\) of \(\mathcal{M}\) defines a collection of fundamental systems of entourages \(\mathfrak{M}(M) = \{\mathcal{B}(d): d\in M\}\).
definition (in muliple_pmetric)
\( \mathfrak{M} (M) = \{\mathcal{B} (d).\ d\in M\} \)
To get a fundamental system of entourages common to all pseudometrics \(d\in \mathcal{M}\) we take intersections of sets selected from finite nonempty subcollections of the collection of all fundamental systems of entourages defined by pseudometrics \(d\in \mathcal{M}\). To distinguish it from the common fundamental system of entourages defined in the previous section we denote that \(\mathfrak{B}_1\).
definition (in muliple_pmetric)
\( \mathfrak{B} _1 \equiv \bigcup M\in \text{FinPow}(\mathcal{M} )\setminus \{\emptyset \}.\ \{(\bigcap B\in \mathfrak{M} (M).\ g(B)).\ g\in \text{ChoiceFunctions}(\mathfrak{M} (M))\} \)
If \(M\) is a nonempty finite subset of \(mathcal{M}\) then we have inclusion \(\{\bigcap_{B\in \mathfrak{M}(M)} g(B) : g \in \mathcal(C)(\mathfrak{M}(M)\} \subseteq \{\bigcap_{d\in M} d^{-1}(\{c\in L^+: c\leq f(d)\}:\ f:M\rightarrow L_+\})\). where \(\mathcal{C}(\mathcal{A})\) is the set of choice functions for a collection \(\mathcal{A}\) (see theory Cardinal_ZF for definition of choice function for a collection.
lemma (in muliple_pmetric) mgauge_alt_mgauge1:
assumes \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \)
defines \( \mathcal{C} \equiv \text{ChoiceFunctions}(\mathfrak{M} (M)) \)
shows \( \{(\bigcap B\in \mathfrak{M} (M).\ g(B)).\ g\in \mathcal{C} \} \subseteq \{(\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})).\ f\in M\rightarrow L_+\} \)proofassumes \( d\in \mathcal{M} \)
shows \( pmetric\_space(L,A,r,d,X) \)assumes \( M\in \text{FinPow}(\mathcal{M} ) \) and \( d\in M \)
shows \( d: X\times X \rightarrow L^+ \)assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \)assumes \( \forall i\in I.\ P(i) \subseteq X \)
shows \( (\bigcap i\in I.\ P(i)) \subseteq X \)assumes \( I\subseteq M \), \( I\neq \emptyset \)
shows \( (\bigcap i\in M.\ P(i)) \subseteq (\bigcap i\in I.\ P(i)) \)assumes \( b_1\leq b_2 \)
shows \( d^{-1}(\{c\in L^+.\ c\leq b_1\}) \subseteq d^{-1}(\{c\in L^+.\ c\leq b_2\}) \)assumes \( r \text{ down-directs } L_+ \)
shows \( \text{IsDownDirectedSet}(L_+,r) \)assumes \( \text{IsDownDirectedSet}(Y,r) \), \( A\in \text{FinPow}(X) \), \( B\in \text{FinPow}(X) \), \( f:A\rightarrow Y \), \( g:B\rightarrow Y \)
shows \( \exists h\in A\cup B\rightarrow Y.\ (\forall x\in A.\ \langle h(x),f(x)\rangle \in r) \wedge (\forall x\in B.\ \langle h(x),g(x)\rangle \in r) \)assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)
shows \( A \cup B \in \text{FinPow}(X) \)assumes \( M_1\subseteq \mathcal{M} \), \( M_1\subseteq M \), \( M_1\neq \emptyset \), \( f_1:M_1\rightarrow L_+ \), \( f:M\rightarrow L_+ \) and \( \forall d\in M_1.\ f(d)\leq f_1(d) \)
shows \( (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \subseteq (\bigcap d\in M_1.\ d^{-1}(\{c\in L^+.\ c\leq f_1(d)\})) \)assumes \( x\in X \) and \( \phi (x) \)
shows \( \exists x\in X.\ \phi (x) \)assumes \( B\in \mathfrak{B} \)
shows \( id(X)\subseteq B \)assumes \( B\in \mathfrak{B} \)
shows \( B = converse(B) \)assumes \( B\in \mathfrak{B} \)
shows \( B\subseteq X\times X \)assumes \( X\neq \emptyset \)
shows \( \text{FinPow}(X)\setminus \{\emptyset \} \neq \emptyset \)assumes \( c\in Y \)
shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \)assumes \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \), \( f:M\rightarrow L_+ \)
shows \( (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \in \mathfrak{B} \)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)) \)assumes \( b_2\in L_+ \) and \( b_2 + b_2 \leq b_1 \)
defines \( B_1 \equiv d^{-1}(\{c\in L^+.\ c\leq b_1\}) \) and \( B_2 \equiv d^{-1}(\{c\in L^+.\ c\leq b_2\}) \)
shows \( B_2\circ B_2 \subseteq B_1 \)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)) \)assumes \( r \text{ down-directs } L_+ \), \( B_1\in \mathfrak{B} \), \( B_2\in \mathfrak{B} \)
shows \( \exists B\in \mathfrak{B} .\ B\subseteq B_1\cap B_2 \)assumes \( B\in \mathfrak{B} \)
shows \( id(X)\subseteq B \), \( B = converse(B) \), \( \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B) \)assumes \( \text{IsHalfable}(L,A,r) \), \( B_1\in \mathfrak{B} \)
shows \( \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1 \)assumes \( \mathcal{M} \neq \emptyset \) and \( L_+\neq \emptyset \)
shows \( \mathfrak{B} \neq \emptyset \)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 \)assumes \( \Phi \text{ is a uniformity on } X \)
shows \( \text{UniformTopology}(\Phi ,X) \text{ is a topology } \) and \( \bigcup \text{UniformTopology}(\Phi ,X) = X \)assumes \( Finite(X) \)
shows \( Finite(\{K(x).\ x\in X\}) \)