IsarMathLib

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

theory MetricUniform_ZF imports FinOrd_ZF_1 MetricSpace_ZF
begin

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 the results proven in this theory are true for the standard real-valued pseudometrics.

Definitions and notation

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 function 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_alt

If \(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) \)proof
from assms, mpmetricAssm show \( \text{IsApseudoMetric}(d,X,L,A,r) \)
qed

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\).

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_def

Members 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 \)proof
from assms obtain \( M \) \( f \) where \( M\in \text{FinPow}(\mathcal{M} ) \) and I: \( B = (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \) using mgauge_def_alt
{
fix \( d \)
assume \( d\in M \)
with \( M\in \text{FinPow}(\mathcal{M} ) \) have \( d: X\times X \rightarrow L^+ \) using each_pmetric_map
then have \( d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \subseteq X\times X \) using func1_1_L15
}
with I show \( thesis \) using inter_subsets_subset
qed

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)\})\).

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)\})) \)proof
let \( L = (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \)
let \( R = (\bigcap d\in M_1.\ d^{-1}(\{c\in L^+.\ c\leq f_1(d)\})) \)
from assms(2,3) have I: \( L \subseteq (\bigcap d\in M_1.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \) using inter_index_mono
from assms(1,6) have \( \forall d\in M_1.\ (d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \subseteq d^{-1}(\{c\in L^+.\ c\leq f_1(d)\}) \) using pmetric_space_valid_in_mpm, uniform_gauge_mono
with assms(2) have \( (\bigcap d\in M_1.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \subseteq R \)
with I show \( L\subseteq R \) by (rule subset_trans )
qed

For 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 \)proof
from assms(2,3) obtain \( M_1 \) \( f_1 \) \( M_2 \) \( f_2 \) where \( M_1\neq \emptyset \), \( M_2\neq \emptyset \) and I: \( M_1\in \text{FinPow}(\mathcal{M} ) \), \( M_2\in \text{FinPow}(\mathcal{M} ) \), \( f_1:M_1\rightarrow L_+ \), \( f_2:M_2\rightarrow L_+ \) and II: \( B_1 = (\bigcap d\in M_1.\ d^{-1}(\{c\in L^+.\ c\leq f_1(d)\})) \), \( B_2 = (\bigcap d\in M_2.\ d^{-1}(\{c\in L^+.\ c\leq f_2(d)\})) \) using mgauge_def_alt
let \( M_3 = M_1\cup M_2 \)
from assms(1) have \( \text{IsDownDirectedSet}(L_+,r) \) using down_directs_directed
with I have \( \exists f_3\in M_3\rightarrow L_+.\ (\forall d\in M_1.\ \langle f_3(d),f_1(d)\rangle \in r) \wedge (\forall d\in M_2.\ \langle f_3(d),f_2(d)\rangle \in r) \) using two_fun_low_bound
then obtain \( f_3 \) where \( f_3:M_3\rightarrow L_+ \) and III: \( \forall d\in M_1.\ f_3(d)\leq f_1(d) \), \( \forall d\in M_2.\ f_3(d)\leq f_2(d) \)
let \( B_3 = \bigcap d\in M_3.\ d^{-1}(\{c\in L^+.\ c\leq f_3(d)\}) \)
from I(1,2), \( M_1\neq \emptyset \), \( f_3:M_3\rightarrow L_+ \) have \( B_3\in \mathfrak{B} \) using union_finpow, mgauge_def_alt
moreover
have \( B_3\subseteq B_1\cap B_2 \)proof
from I(1,2) have \( M_1\subseteq \mathcal{M} \), \( M_1\subseteq M_3 \), \( M_2\subseteq \mathcal{M} \), \( M_2\subseteq M_3 \) unfolding FinPow_def
with \( M_1\neq \emptyset \), \( M_2\neq \emptyset \), I(3,4), II, \( f_3:M_3\rightarrow L_+ \), III have \( B_3\subseteq B_1 \) and \( B_3\subseteq B_2 \) using fun_inter_vimage_mono
thus \( B_3\subseteq B_1\cap B_2 \)
qed
ultimately show \( \exists B\in \mathfrak{B} .\ B\subseteq B_1\cap B_2 \) by (rule witness_exists )
qed

Sets 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
from assms obtain \( M \) \( f \) where \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \), \( f:M\rightarrow L_+ \) and I: \( B = (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \) using mgauge_def_alt
{
fix \( d \)
assume \( d\in M \)
let \( B_d = d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \)
from \( d\in M \), \( f:M\rightarrow L_+ \), \( M\in \text{FinPow}(\mathcal{M} ) \) have \( pmetric\_space(L,A,r,d,X) \) and \( B_d \in \text{UniformGauge}(X,L,A,r,d) \) unfolding FinPow_def, UniformGauge_def using apply_funtype, pmetric_space_valid_in_mpm
then have \( id(X)\subseteq B_d \) and \( B_d = converse(B_d) \) using gauge_2nd_cond, gauge_symmetric
}
with I, \( M\neq \emptyset \) show \( id(X)\subseteq B \) and \( B = converse(B) \)
from assms, \( B = converse(B) \) show \( \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B) \)
qed

\(\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_relations

If \(\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 \)proof
from assms obtain \( M \) \( y \) where \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \) and \( y\in L_+ \) using finpow_nempty_nempty
from \( y\in L_+ \) have \( \text{ConstantFunction}(M,y):M\rightarrow L_+ \) using func1_3_L1
with \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \) show \( \mathfrak{B} \neq \emptyset \) using mgauge_finset_fun
qed

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\).

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 \)proof
from assms(2) obtain \( M \) \( f_1 \) where \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \), \( f_1:M\rightarrow L_+ \) and I: \( B_1 = (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f_1(d)\})) \) using mgauge_def_alt
from assms(1), \( f_1:M\rightarrow L_+ \) have \( \forall d\in M.\ \exists b_2\in L_+.\ b_2 + b_2 \leq f_1(d) \) using apply_funtype unfolding IsHalfable_def
with \( M\in \text{FinPow}(\mathcal{M} ) \) have \( \exists f_2\in M\rightarrow L_+.\ \forall d\in M.\ f_2(d) + f_2(d) \leq f_1(d) \) unfolding FinPow_def using finite_choice_fun
then obtain \( f_2 \) where \( f_2\in M\rightarrow L_+ \) and II: \( \forall d\in M.\ f_2(d) + f_2(d) \leq f_1(d) \)
let \( B_2 = \bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f_2(d)\}) \)
{
fix \( d \)
assume \( d\in M \)
let \( A_2 = d^{-1}(\{c\in L^+.\ c\leq f_2(d)\}) \)
from \( d\in M \), \( M\in \text{FinPow}(\mathcal{M} ) \) have \( pmetric\_space(L,A,r,d,X) \) unfolding FinPow_def using pmetric_space_valid_in_mpm
with \( f_2\in M\rightarrow L_+ \), \( d\in M \), II have \( A_2\circ A_2 \subseteq d^{-1}(\{c\in L^+.\ c\leq f_1(d)\}) \) using apply_funtype, half_vimage_square
}
with \( M\neq \emptyset \), I have \( B_2\circ B_2 \subseteq B_1 \) using square_incl_product
with \( M\in \text{FinPow}(\mathcal{M} ) \), \( M\neq \emptyset \), \( f_2\in M\rightarrow L_+ \) show \( thesis \) using mgauge_finset_fun
qed
end
Definition of UniformGaugeSets: \( \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)\} \)
Definition of UniformGauges: \( \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) \)
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_+\}) \)
lemma (in muliple_pmetric) pmetric_space_valid_in_mpm:

assumes \( d\in \mathcal{M} \)

shows \( pmetric\_space(L,A,r,d,X) \)
lemma (in pmetric_space) pmetric_properties: shows \( d: X\times X \rightarrow L^+ \), \( \forall x\in X.\ d\langle x,x\rangle = 0 \), \( \forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = d\langle y,x\rangle \), \( \forall x\in X.\ \forall y\in X.\ \forall z\in X.\ d\langle x,z\rangle \leq d\langle x,y\rangle + d\langle y,z\rangle \)
Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
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^+ \)
lemma func1_1_L15:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \)
lemma inter_subsets_subset:

assumes \( \forall i\in I.\ P(i) \subseteq X \)

shows \( (\bigcap i\in I.\ P(i)) \subseteq X \)
lemma inter_index_mono:

assumes \( I\subseteq M \), \( I\neq \emptyset \)

shows \( (\bigcap i\in M.\ P(i)) \subseteq (\bigcap i\in I.\ P(i)) \)
lemma (in pmetric_space) uniform_gauge_mono:

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\}) \)
lemma (in loop1) down_directs_directed:

assumes \( r \text{ down-directs } L_+ \)

shows \( \text{IsDownDirectedSet}(L_+,r) \)
lemma two_fun_low_bound:

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) \)
lemma union_finpow:

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

shows \( A \cup B \in \text{FinPow}(X) \)
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)\})) \)
lemma witness_exists:

assumes \( x\in X \) and \( \phi (x) \)

shows \( \exists x\in X.\ \phi (x) \)
Definition of UniformGauge: \( \text{UniformGauge}(X,L,A,r,d) \equiv \{d^{-1}(\{c\in \text{Nonnegative}(L,A,r).\ \langle c,b\rangle \in r\}).\ b\in \text{PositiveSet}(L,A,r)\} \)
lemma (in pmetric_space) gauge_2nd_cond:

assumes \( B\in \mathfrak{B} \)

shows \( id(X)\subseteq B \)
lemma (in pmetric_space) gauge_symmetric:

assumes \( B\in \mathfrak{B} \)

shows \( B = converse(B) \)
lemma (in muliple_pmetric) muniform_gauge_relations:

assumes \( B\in \mathfrak{B} \)

shows \( B\subseteq X\times X \)
lemma finpow_nempty_nempty:

assumes \( X\neq \emptyset \)

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

assumes \( c\in Y \)

shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \)
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} \)
Definition of IsHalfable: \( \text{IsHalfable}(L,A,r) \equiv \forall b_1\in \text{PositiveSet}(L,A,r).\ \exists b_2\in \text{PositiveSet}(L,A,r).\ \langle A\langle b_2,b_2\rangle ,b_1\rangle \in r \)
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 (in pmetric_space) half_vimage_square:

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 \)
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)) \)