IsarMathLib

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

theory MetricUniform_ZF imports FinOrd_ZF_1 MetricSpace_ZF
begin

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.

From collection of pseudometrics to fundamental system of entourages

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_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

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

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_def

An alternative approach

The 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_+\} \)proof
let \( L = \{(\bigcap B\in \mathfrak{M} (M).\ g(B)).\ g\in \mathcal{C} \} \)
let \( R = \{(\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})).\ f\in M\rightarrow L_+\} \)
from assms(1,2) have \( Finite(\mathfrak{M} (M)) \) and \( \mathfrak{M} (M)\neq \emptyset \) unfolding gauge_set_def, FinPow_def using fin_rep_fin
{
fix \( U \)
assume \( U \in L \)
then obtain \( g \) where \( g\in \mathcal{C} \) and \( U=(\bigcap B\in \mathfrak{M} (M).\ g(B)) \)
from assms(3), \( g\in \mathcal{C} \) have \( g:(\mathfrak{M} (M))\rightarrow (\bigcup \mathfrak{M} (M)) \) and I: \( \forall B\in \mathfrak{M} (M).\ g(B) \in B \) unfolding ChoiceFunctions_def
{
fix \( d \)
assume \( d\in M \)
then have \( \mathcal{B} (d) \in \mathfrak{M} (M) \) and II: \( \mathcal{B} (d) = \{d^{-1}(\{c\in L^+.\ c\leq b\}).\ b\in L_+\} \) unfolding gauge_set_def, gauge_def
from I, \( \mathcal{B} (d) \in \mathfrak{M} (M) \) have \( g(\mathcal{B} (d)) \in \mathcal{B} (d) \)
with II obtain \( b \) where \( b\in L_+ \) and \( g(\mathcal{B} (d)) = d^{-1}(\{c\in L^+.\ c\leq b\}) \)
hence \( \exists b\in L_+.\ g(\mathcal{B} (d)) = d^{-1}(\{c\in L^+.\ c\leq b\}) \)
}
hence \( \forall d\in M.\ \exists b\in L_+.\ g(\mathcal{B} (d)) = d^{-1}(\{c\in L^+.\ c\leq b\}) \)
with assms(1) have \( \exists f\in M\rightarrow L_+.\ \forall d\in M.\ g(\mathcal{B} (d)) = d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \) unfolding FinPow_def using finite_choice_fun
then obtain \( f \) where \( f:M\rightarrow L_+ \) and II: \( \forall d\in M.\ g(\mathcal{B} (d)) = d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \)
have \( U = (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \)proof
{
fix \( p \)
assume \( p\in U \)
with \( U=(\bigcap B\in \mathfrak{M} (M).\ g(B)) \) have \( \forall B\in \mathfrak{M} (M).\ p\in g(B) \)
{
fix \( d \)
assume \( d\in M \)
then have \( \mathcal{B} (d) \in \mathfrak{M} (M) \) unfolding gauge_set_def
with \( \forall B\in \mathfrak{M} (M).\ p\in g(B) \) have \( p\in g(\mathcal{B} (d)) \)
with II, \( d\in M \) have \( p \in d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \)
}
hence \( \forall d\in M.\ p \in d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \)
with assms(2) have \( p\in (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \)
}
thus \( U \subseteq (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \)
{
fix \( p \)
assume \( p \in (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \)
hence III: \( \forall d\in M.\ p \in d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \)
{
fix \( B \)
assume \( B\in \mathfrak{M} (M) \)
then have \( B \in \{\mathcal{B} (d).\ d\in M\} \) unfolding gauge_set_def
then obtain \( d \) where \( d\in M \) and \( B=\mathcal{B} (d) \) unfolding gauge_def
from \( d\in M \), II have \( g(\mathcal{B} (d)) = d^{-1}(\{c\in L^+.\ c\leq f(d)\}) \)
with III, \( d\in M \) have \( p \in g(\mathcal{B} (d)) \)
with \( B=\mathcal{B} (d) \) have \( p\in g(B) \)
}
hence \( \forall B\in \mathfrak{M} (M).\ p\in g(B) \)
with \( \mathfrak{M} (M)\neq \emptyset \), \( U=(\bigcap B\in \mathfrak{M} (M).\ g(B)) \) have \( p\in U \)
}
thus \( (\bigcap d\in M.\ d^{-1}(\{c\in L^+.\ c\leq f(d)\})) \subseteq U \)
qed
with \( f:M\rightarrow L_+ \) have \( U\in R \)
}
thus \( L\subseteq R \)
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)) \)
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 \)
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) \)
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 \)
lemma (in muliple_pmetric) mgauge_5thCond: shows \( \mathfrak{B} \subseteq Pow(X\times X) \)
lemma (in muliple_pmetric) mgauge_6thCond:

assumes \( \mathcal{M} \neq \emptyset \) and \( L_+\neq \emptyset \)

shows \( \mathfrak{B} \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 \)
Definition of gauge_set: \( \mathfrak{M} (M) = \{\mathcal{B} (d).\ d\in M\} \)
lemma fin_rep_fin:

assumes \( Finite(X) \)

shows \( Finite(\{K(x).\ x\in X\}) \)
Definition of ChoiceFunctions: \( \text{ChoiceFunctions}(\mathcal{A} ) \equiv \{f\in \mathcal{A} \rightarrow \bigcup \mathcal{A} .\ \forall A\in \mathcal{A} .\ f(A)\in A\} \)
Definition of gauge: \( \mathcal{B} (d) \equiv \{d^{-1}(\{c\in L^+.\ c\leq b\}).\ b\in L_+\} \)