IsarMathLib

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

theory MetricSpace_ZF imports Topology_ZF_1 OrderedLoop_ZF Lattice_ZF UniformSpace_ZF
begin

A metric space is a set on which a distance between points is defined as a function \(d:X \times X \to [0,\infty)\). With this definition each metric space is a topological space which is paracompact and Hausdorff (\(T_2\)), hence normal (in fact even perfectly normal).

Pseudometric - definition and basic properties

A metric on \(X\) is usually defined as a function \(d:X \times X \to [0,\infty)\) that satisfies the conditions \(d(x,x) = 0\), \(d(x, y) = 0 \Rightarrow x = y\) (identity of indiscernibles), \(d(x, y) = d(y, x)\) (symmetry) and \(d(x, y) \le d(x, z) + d(z, y)\) (triangle inequality) for all \(x,y \in X\). Here we are going to be a bit more general and define metric and pseudo-metric as a function valued in an ordered loop.

First we define a pseudo-metric, which has the axioms of a metric, but without the second part of the identity of indiscernibles. In our definition IsApseudoMetric is a predicate on five sets: the function \(d\), the set \(X\) on which the metric is defined, the loop carrier \(G\), the loop operation \(A\) and the order \(r\) on \(G\).

definition

\( \text{IsApseudoMetric}(d,X,G,A,r) \equiv d:X\times X \rightarrow \text{Nonnegative}(G,A,r) \) \( \wedge (\forall x\in X.\ d\langle x,x\rangle = \text{ TheNeutralElement}(G,A))\) \( \wedge (\forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = d\langle y,x\rangle )\) \( \wedge (\forall x\in X.\ \forall y\in X.\ \forall z\in X.\ \langle d\langle x,z\rangle , A\langle d\langle x,y\rangle ,d\langle y,z\rangle \rangle \rangle \in r) \)

We add the full axiom of identity of indiscernibles to the definition of a pseudometric to get the definition of metric.

definition

\( \text{IsAmetric}(d,X,G,A,r) \equiv \) \( \text{IsApseudoMetric}(d,X,G,A,r) \wedge (\forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = \text{ TheNeutralElement}(G,A) \longrightarrow x=y) \)

A disk is defined as set of points located less than the radius from the center.

definition

\( \text{Disk}(X,d,r,c,R) \equiv \{x\in X.\ \langle d\langle c,x\rangle ,R\rangle \in \text{StrictVersion}(r)\} \)

We define metric topology as consisting of unions of open disks.

definition

\( \text{MetricTopology}(X,L,A,r,d) \equiv \{\bigcup \mathcal{A} .\ \mathcal{A} \in Pow(\bigcup c\in X.\ \{ \text{Disk}(X,d,r,c,R).\ R\in \text{PositiveSet}(L,A,r)\})\} \)

Next we define notation for metric spaces. We will reuse the additive notation defined in the loop1 locale adding only the assumption about \(d\) being a pseudometric and notation for a disk centered at \(c\) with radius \(R\). Since for many theorems it is sufficient to assume the pseudometric axioms we will assume in this context that the sets \(d,X,L,A,r\) form a pseudometric raher than a metric. In the pmetric_space context \(\tau\) denotes the topology defined by the metric \(d\). Analogously to the notation defined in the topology0 context \( int(A) \), \( cl(A) \), \( \partial A \) will denote the interior, closure and boundary of the set \(A\) with respect to the metric topology.

locale pmetric_space = loop1 +

assumes pmetricAssum: \( \text{IsApseudoMetric}(d,X,L,A,r) \)

defines \( disk(c,R) \equiv \text{Disk}(X,d,r,c,R) \)

defines \( \tau \equiv \text{MetricTopology}(X,L,A,r,d) \)

defines \( int(D) \equiv \text{Interior}(D,\tau ) \)

defines \( cl(D) \equiv \text{Closure}(D,\tau ) \)

The next lemma shows the definition of the pseudometric in the notation used in the pmetric_space context.

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 \) using pmetricAssum unfolding IsApseudoMetric_def

The values of the metric are in the in the nonnegative set of the loop, hence in the loop.

lemma (in pmetric_space) pmetric_loop_valued:

assumes \( x\in X \), \( y\in X \)

shows \( d\langle x,y\rangle \in L^+ \), \( d\langle x,y\rangle \in L \)proof
from assms show \( d\langle x,y\rangle \in L^+ \) using pmetric_properties(1), apply_funtype
then show \( d\langle x,y\rangle \in L \) using Nonnegative_def
qed

The definition of the disk in the notation used in the pmetric_space context:

lemma (in pmetric_space) disk_definition:

shows \( disk(c,R) = \{x\in X.\ d\langle c,x\rangle \lt R\} \)proof
have \( disk(c,R) = \text{Disk}(X,d,r,c,R) \)
then have \( disk(c,R) = \{x\in X.\ \langle d\langle c,x\rangle ,R\rangle \in \text{StrictVersion}(r)\} \) unfolding Disk_def
moreover
have \( \forall x\in X.\ \langle d\langle c,x\rangle ,R\rangle \in \text{StrictVersion}(r) \longleftrightarrow d\langle c,x\rangle \lt R \) using def_of_strict_ver
ultimately show \( thesis \)
qed

If the radius is positive then the center is in disk.

lemma (in pmetric_space) center_in_disk:

assumes \( c\in X \) and \( R\in L_+ \)

shows \( c \in disk(c,R) \) using pmetricAssum, assms, IsApseudoMetric_def, PositiveSet_def, disk_definition

A technical lemma that allows us to shorten some proofs: if \(c\) is an element of \(X\) and \(x\) is in disk with center \(c\) and radius \(R\) then \(R\) is a positive element of \(L\) and \(-d(x,y)+R\) is in the set of positive elements of the loop.

lemma (in pmetric_space) radius_in_loop:

assumes \( c\in X \) and \( x \in disk(c,R) \)

shows \( R\in L \), \( 0 \lt R \), \( R\in L_+ \), \( ( - d\langle c,x\rangle + R) \in L_+ \)proof
from assms(2) have \( x\in X \) and \( d\langle c,x\rangle \lt R \) using disk_definition
with assms(1) show \( 0 \lt R \) using pmetric_properties(1), apply_funtype, nonneg_definition, loop_strict_ord_trans
then show \( R\in L \) and \( R\in L_+ \) using posset_definition, PositiveSet_def
from \( d\langle c,x\rangle \lt R \) show \( ( - d\langle c,x\rangle + R) \in L_+ \) using ls_other_side(2)
qed

If a point \(x\) is inside a disk \(B\) and \(m\leq -d\langle c,x\rangle + R\) then the disk centered at the point \(x\) and with radius \(m\) is contained in the disk \(B\).

lemma (in pmetric_space) disk_in_disk:

assumes \( c\in X \) and \( x \in disk(c,R) \) and \( m \leq ( - d\langle c,x\rangle + R) \)

shows \( disk(x,m) \subseteq disk(c,R) \)proof
fix \( y \)
assume \( y \in disk(x,m) \)
then have \( d\langle x,y\rangle \lt m \) using disk_definition
from assms(1,2), \( y \in disk(x,m) \) have \( R\in L \), \( x\in X \), \( y\in X \) using radius_in_loop(1), disk_definition
with assms(1) have \( d\langle c,y\rangle \leq d\langle c,x\rangle + d\langle x,y\rangle \) using pmetric_properties(4)
from assms(1), \( x\in X \) have \( d\langle c,x\rangle \in L \) using pmetric_properties(1), apply_funtype, nonneg_subset
with \( d\langle x,y\rangle \lt m \), assms(3) have \( d\langle c,x\rangle + d\langle x,y\rangle \lt d\langle c,x\rangle + ( - d\langle c,x\rangle + R) \) using loop_strict_ord_trans1, strict_ord_trans_inv(2)
with \( d\langle c,x\rangle \in L \), \( R\in L \), \( d\langle c,y\rangle \leq d\langle c,x\rangle + d\langle x,y\rangle \), \( y\in X \) show \( y \in disk(c,R) \) using lrdiv_props(6), loop_strict_ord_trans, disk_definition
qed

A special case of disk_in_disk where we set \(m = -d\langle c,x\rangle + R\): if \(x\) is an element of a disk with center \(c\in X\) and radius \(R\) then this disk contains the disk centered at \(x\) and with radius \(-d\langle c,x\rangle + R\).

lemma (in pmetric_space) disk_in_disk1:

assumes \( c\in X \) and \( x \in disk(c,R) \)

shows \( disk(x, - d\langle c,x\rangle + R) \subseteq disk(c,R) \)proof
from assms(2) have \( R\in L \) and \( d\langle c,x\rangle \in L \) using disk_definition, less_members
with assms show \( thesis \) using left_right_sub_closed(1), loop_ord_refl, disk_in_disk
qed

Assuming that two disks have the same center, closed disk with smaller radius in contained in the (open) disk with a larger radius.

lemma (in pmetric_space) disk_radius_strict_mono:

assumes \( r_1 \lt r_2 \)

shows \( \{y\in X.\ d\langle x,y\rangle \leq r_1\} \subseteq disk(x,r_2) \) using assms, loop_strict_ord_trans, disk_definition

If we assume that the loop's order relation down-directs \(L_+\) then the collection of disks centered at points of the space and with radii in the positive set of the loop satisfies the base condition. The property that an order relation "down-directs" a set is defined in Order_ZF and means that every two-element subset of the set has a lower bound in that set.

lemma (in pmetric_space) disks_form_base:

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

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( B \text{ satisfies the base condition } \)proof
{
fix \( U \) \( V \)
assume \( U\in B \), \( V\in B \)
fix \( x \)
assume \( x\in U\cap V \)
have \( \exists W\in B.\ x\in W \wedge W\subseteq U\cap V \)proof
from assms(2), \( U\in B \), \( V\in B \) obtain \( c_U \) \( c_V \) \( R_U \) \( R_V \) where \( c_U \in X \), \( R_U \in L_+ \), \( c_V \in X \), \( R_V \in L_+ \), \( U = disk(c_U,R_U) \), \( V = disk(c_V,R_V) \)
with \( x\in U\cap V \) have \( x \in disk(c_U,R_U) \) and \( x \in disk(c_V,R_V) \)
then have \( x\in X \), \( d\langle c_U,x\rangle \lt R_U \), \( d\langle c_V,x\rangle \lt R_V \) using disk_definition
let \( m_U = - d\langle c_U,x\rangle + R_U \)
let \( m_V = - d\langle c_V,x\rangle + R_V \)
from \( c_U\in X \), \( x\in disk(c_U,R_U) \), \( c_V\in X \), \( x\in disk(c_V,R_V) \) have \( m_U\in L_+ \) and \( m_V\in L_+ \) using radius_in_loop(4)
with assms(1) obtain \( m \) where \( m \in L_+ \), \( m \leq m_U \), \( m \leq m_V \) unfolding DownDirects_def
let \( W = disk(x,m) \)
from \( m \in L_+ \), \( m \leq m_U \), \( m \leq m_V \), \( c_U \in X \), \( x \in disk(c_U,R_U) \), \( c_V \in X \), \( x \in disk(c_V,R_V) \), \( U = disk(c_U,R_U) \), \( V = disk(c_V,R_V) \) have \( W \subseteq U\cap V \) using disk_in_disk
moreover
from assms(2), \( x\in X \), \( m \in L_+ \) have \( W \in B \) and \( x\in W \) using center_in_disk
ultimately show \( thesis \)
qed
}
then show \( thesis \) unfolding SatisfiesBaseCondition_def
qed

Disks centered at points farther away than the sum of radii do not overlap.

lemma (in pmetric_space) far_disks:

assumes \( x\in X \), \( y\in X \), \( r_x + r_y \leq d\langle x,y\rangle \)

shows \( disk(x,r_x)\cap disk(y,r_y) = \emptyset \)proof
{
assume \( disk(x,r_x)\cap disk(y,r_y) \neq \emptyset \)
then obtain \( z \) where \( z \in disk(x,r_x)\cap disk(y,r_y) \)
then have \( z\in X \) and \( d\langle x,z\rangle + d\langle y,z\rangle \lt r_x + r_y \) using disk_definition, add_ineq_strict
moreover
from assms(1,2), \( z\in X \) have \( d\langle x,y\rangle \leq d\langle x,z\rangle + d\langle y,z\rangle \) using pmetric_properties(3,4)
ultimately have \( d\langle x,y\rangle \lt r_x + r_y \) using loop_strict_ord_trans
with assms(3) have \( False \) using loop_strict_ord_trans
}
thus \( thesis \)
qed

If we have a loop element that is smaller than the distance between two points, then we can separate these points with disks.

lemma (in pmetric_space) disjoint_disks:

assumes \( x\in X \), \( y\in X \), \( r_x \lt d\langle x,y\rangle \)

shows \( ( - r_x + (d\langle x,y\rangle )) \in L_+ \) and \( disk(x,r_x)\cap disk(y, - r_x + (d\langle x,y\rangle )) = 0 \)proof
from assms(3) show \( ( - r_x + (d\langle x,y\rangle )) \in L_+ \) using ls_other_side, posset_definition1
from assms(1,2,3) have \( r_x\in L \) and \( d\langle x,y\rangle \in L \) using less_members(1), pmetric_loop_valued(2)
then have \( r_x + ( - r_x + (d\langle x,y\rangle )) = d\langle x,y\rangle \) using lrdiv_props(6)
with assms(1,2), \( d\langle x,y\rangle \in L \) show \( disk(x,r_x)\cap disk(y, - r_x + (d\langle x,y\rangle )) = 0 \) using loop_ord_refl, far_disks
qed

The definition of metric topology written in notation of pmetric_space context:

lemma (in pmetric_space) metric_top_def_alt:

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( \tau = \{\bigcup A.\ A \in Pow(B)\} \)proof
from assms have \( \text{MetricTopology}(X,L,A,r,d) = \{\bigcup A.\ A \in Pow(B)\} \) unfolding MetricTopology_def
thus \( thesis \)
qed

If the order of the loop down-directs its set of positive elements then the metric topology defined as collection of unions of (open) disks is indeed a topology. Recall that in the pmetric_space context \(\tau\) denotes the metric topology.

theorem (in pmetric_space) pmetric_is_top:

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

shows \( \tau \text{ is a topology } \) using assms, disks_form_base, Top_1_2_T1, metric_top_def_alt

If \(r\) down-directs \(L_+\) then the collection of open disks is a base for the metric topology.

theorem (in pmetric_space) disks_are_base:

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

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( B \text{ is a base for } \tau \) using assms, disks_form_base, Top_1_2_T1, metric_top_def_alt

If \(r\) down-directs \(L_+\) then \(X\) is the carrier of metric topology.

theorem (in pmetric_space) metric_top_carrier:

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

shows \( \bigcup \tau = X \)proof
let \( B = \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)
from assms have \( \bigcup \tau = \bigcup B \) using disks_are_base, Top_1_2_L5
moreover
have \( \bigcup B = X \)proof
show \( \bigcup B \subseteq X \) using disk_definition
from assms show \( X \subseteq \bigcup B \) unfolding DownDirects_def using center_in_disk
qed
ultimately show \( \bigcup \tau = X \)
qed

Under the assumption that \(r\) down-directs \(L_+\) the propositions proven in the topology0 context can be used in the pmetric_space context.

lemma (in pmetric_space) topology0_valid_in_pmetric_space:

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

shows \( topology0(\tau ) \) using assms, pmetric_is_top unfolding topology0_def

If \(r\) down-directs \(L_+\) then disks are open in the metric topology.

lemma (in pmetric_space) disks_open:

assumes \( c\in X \), \( R\in L_+ \), \( r \text{ down-directs } L_+ \)

shows \( disk(c,R) \in \tau \) using assms, base_sets_open, disks_are_base(1), pmetric_is_top

To define the metric_space locale we take the pmetric_space and add the assumption of identity of indiscernibles.

locale metric_space = pmetric_space +

assumes ident_indisc: \( \forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = 0 \longrightarrow x=y \)

In the metric_space locale \(d\) is a metric.

lemma (in metric_space) d_metric:

shows \( \text{IsAmetric}(d,X,L,A,r) \) using pmetricAssum, ident_indisc unfolding IsAmetric_def

Distance of different points is greater than zero.

lemma (in metric_space) dist_pos:

assumes \( x\in X \), \( y\in X \), \( x\neq y \)

shows \( 0 \lt d\langle x,y\rangle \), \( d\langle x,y\rangle \in L_+ \)proof
from assms(1,2) have \( d\langle x,y\rangle \in L^+ \) using pmetric_properties(1), apply_funtype
then have \( 0 \leq d\langle x,y\rangle \) using Nonnegative_def
with assms show \( d\langle x,y\rangle \in L_+ \) and \( 0 \lt d\langle x,y\rangle \) using ident_indisc, posset_definition, posset_definition1
qed

If \(r\) down-directs \(L_+\) then the ordered loop valued metric space is \(T_2\) (i.e. Hausdorff).

theorem (in metric_space) metric_space_T2:

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

shows \( \tau \text{ is }T_2 \)proof
let \( B = \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)
{
fix \( x \) \( y \)
assume \( x\in \bigcup \tau \), \( y\in \bigcup \tau \), \( x\neq y \)
from assms have \( B\subseteq \tau \) using metric_top_def_alt
have \( \exists U\in B.\ \exists V\in B.\ x\in U \wedge y\in V \wedge U\cap V = \emptyset \)proof
let \( R = d\langle x,y\rangle \)
from assms have \( \bigcup \tau = X \) using metric_top_carrier
with \( x\in \bigcup \tau \) have \( x\in X \)
from \( \bigcup \tau = X \), \( y\in \bigcup \tau \) have \( y\in X \)
with \( x\neq y \), \( x\in X \) have \( R\in L_+ \) using dist_pos
with \( x\in X \), \( y\in X \) have \( disk(x,R) \in B \) and \( disk(y,R) \in B \)
{
assume \( disk(x,R) \cap disk(y,R) = \emptyset \)
moreover
from \( x\in X \), \( y\in X \), \( R\in L_+ \) have \( disk(x,R)\in B \), \( disk(y,R)\in B \), \( x\in disk(x,R) \), \( y\in disk(y,R) \) using center_in_disk
ultimately have \( \exists U\in B.\ \exists V\in B.\ x\in U \wedge y\in V \wedge U\cap V = 0 \)
}
moreover {
assume \( disk(x,R) \cap disk(y,R) \neq 0 \)
then obtain \( z \) where \( z \in disk(x,R) \) and \( z \in disk(y,R) \)
then have \( d\langle x,z\rangle \lt R \) using disk_definition
then have \( 0 \lt - d\langle x,z\rangle + R \) using ls_other_side(1)
let \( r = - d\langle x,z\rangle + R \)
have \( r \lt R \)proof
from \( z \in disk(y,R) \), \( x\in X \), \( y\in X \) have \( z\in X \), \( x\neq z \) using disk_definition, pmetric_properties(3)
with \( x\in X \), \( y\in X \), \( z\in X \) show \( thesis \) using pmetric_loop_valued, dist_pos(1), add_subtract_pos(2)
qed
with \( x\in X \), \( y\in X \) have \( disk(x,r)\cap disk(y, - r + R) = 0 \) by (rule disjoint_disks )
moreover
from \( 0 \lt r \), \( r \lt R \) have \( r\in L_+ \), \( ( - r + R) \in L_+ \) using ls_other_side, posset_definition1
with \( x\in X \), \( y\in X \) have \( disk(x,r)\in B \), \( disk(y, - r + (d\langle x,y\rangle ))\in B \) and \( x\in disk(x,r) \), \( y\in disk(y, - r + (d\langle x,y\rangle )) \) using center_in_disk
ultimately have \( \exists U\in B.\ \exists V\in B.\ x\in U \wedge y\in V \wedge U\cap V = 0 \)
} ultimately show \( thesis \)
qed
with \( B\subseteq \tau \) have \( \exists U\in \tau .\ \exists V\in \tau .\ x\in U \wedge y\in V \wedge U\cap V = \emptyset \) by (rule exist2_subset )
}
then show \( thesis \) unfolding isT2_def
qed

Uniform structures on metric spaces

Each pseudometric space with pseudometric \(d:X\times X\rightarrow L^+\) supports a natural uniform structure, defined as supersets of the collection of inverse images \(U_c = d^{-1}([0,c])\), where \(c>0\).

In the following definition \(X\) is the underlying space, \(L\) is the loop (carrier), \(A\) is the loop operation, \(r\) is an order relation compatible with \(A\), and \(d\) is a pseudometric on \(X\), valued in the ordered loop \(L\). With this we define the uniform gauge as the collection of inverse images of the closed intervals \([0,c]\) as \(c\) varies of the set of positive elements of \(L\).

definition

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

In the pmetric_space context we will write \( \text{UniformGauge}(X,L,A,r,d) \) as \( \mathfrak{B} \).

abbreviation (in pmetric_space)

\( \mathfrak{B} \equiv \text{UniformGauge}(X,L,A,r,d) \)

In notation defined in the pmetric_space context we can write the uniform gauge as \(\{ d^{-1}(\{c\in L^+: c\leq b\}: b \in L_+ \}\).

lemma (in pmetric_space) uniform_gauge_def_alt:

shows \( \mathfrak{B} = \{d^{-1}(\{c\in L^+.\ c\leq b\}).\ b\in L_+\} \) unfolding UniformGauge_def

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

lemma (in pmetric_space) uniform_gauge_relations:

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

shows \( B\subseteq X\times X \) using assms, uniform_gauge_def_alt, pmetric_properties(1), func1_1_L3

If the distance between two points of \(X\) is less or equal \(b\), then this pair of points is in \(d^{-1}([0,b])\).

lemma (in pmetric_space) gauge_members:

assumes \( x\in X \), \( y\in X \), \( d\langle x,y\rangle \leq b \)

shows \( \langle x,y\rangle \in d^{-1}(\{c\in L^+.\ c\leq b\}) \) using assms, pmetric_properties(1), apply_funtype, func1_1_L15

Suppose \(b\in L_+\) (i.e. b is an element of the loop that is greater than the neutral element) and \(x\in X\). Then the image of the singleton set \(\{ x\}\) by the relation \(B=\{ d^{-1}(\{c\in L^+: c\leq b\}\) is the set \(\{ y\in X:d\langle x,y\rangle \leq b\}\), i.e. the closed disk with center \(x\) and radius \(b\). Hence the the image \(B\{ x\}\) contains the open disk with center \(x\) and radius \(b\).

lemma (in pmetric_space) disk_in_gauge:

assumes \( b\in L_+ \), \( x\in X \)

defines \( B \equiv d^{-1}(\{c\in L^+.\ c\leq b\}) \)

shows \( B\{x\} = \{y\in X.\ d\langle x,y\rangle \leq b\} \) and \( disk(x,b) \subseteq B\{x\} \)proof
from assms(1,3) have \( B\subseteq X\times X \) using uniform_gauge_def_alt, uniform_gauge_relations
with assms(2,3) show \( B\{x\} = \{y\in X.\ d\langle x,y\rangle \leq b\} \) using pmetric_properties(1), func1_1_L15
then show \( disk(x,b) \subseteq B\{x\} \) using disk_definition
qed

Gauges corresponding to larger elements of the loop are larger.

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\}) \) using ordLoopAssum, assms, vimage_mono1 unfolding IsAnOrdLoop_def, IsPartOrder_def, trans_def

For any two sets of the form \(d^{-1}([0,b])\) we can find a third one that is contained in both.

lemma (in pmetric_space) gauge_1st_cond:

assumes \( r \text{ down-directs } L_+ \), \( B_1\in \mathfrak{B} \), \( B_2\in \mathfrak{B} \)

shows \( \exists B_3\in \mathfrak{B} .\ B_3\subseteq B_1\cap B_2 \)proof
from assms(2,3) obtain \( b_1 \) \( b_2 \) where \( b_1\in L_+ \), \( b_2\in L_+ \) and I: \( B_1 = d^{-1}(\{c\in L^+.\ c\leq b_1\}) \), \( B_2 = d^{-1}(\{c\in L^+.\ c\leq b_2\}) \) using uniform_gauge_def_alt
from assms(1), \( b_1\in L_+ \), \( b_2\in L_+ \) obtain \( b_3 \) where \( b_3\in L_+ \), \( b_3\leq b_1 \), \( b_3\leq b_2 \) unfolding DownDirects_def
from I, \( b_3\leq b_1 \), \( b_3\leq b_2 \) have \( d^{-1}(\{c\in L^+.\ c\leq b_3\}) \subseteq B_1\cap B_2 \) using uniform_gauge_mono
with \( b_3\in L_+ \) show \( thesis \) using uniform_gauge_def_alt
qed

Sets of the form \(d^{-1}([0,b])\) contain the diagonal.

lemma (in pmetric_space) gauge_2nd_cond:

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

shows \( id(X)\subseteq B \)proof
fix \( p \)
assume \( p\in id(X) \)
then obtain \( x \) where \( x\in X \) and \( p=\langle x,x\rangle \)
then have \( p\in X\times X \) and \( d(p) = 0 \) using pmetric_properties(2)
from assms obtain \( b \) where \( b\in L_+ \) and \( B = d^{-1}(\{c\in L^+.\ c\leq b\}) \) using uniform_gauge_def_alt
with \( p\in X\times X \), \( d(p) = 0 \) show \( p\in B \) using posset_definition1, loop_zero_nonneg, pmetric_properties(1), func1_1_L15
qed

Sets of the form \(d^{-1}([0,b])\) are symmetric.

lemma (in pmetric_space) gauge_symmetric:

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

shows \( B = converse(B) \)proof
from assms obtain \( b \) where \( B = d^{-1}(\{c\in L^+.\ c\leq b\}) \) using uniform_gauge_def_alt
with pmetricAssum show \( thesis \) unfolding IsApseudoMetric_def using symm_vimage_symm
qed

A set of the form \(d^{-1}([0,b])\) contains a symmetric set of this form.

corollary (in pmetric_space) gauge_3rd_cond:

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

shows \( \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1) \) using assms, gauge_symmetric

The collection of sets of the form \(d^{-1}([0,b])\) for \(b\in L_+\) is contained of the powerset of \(X\times X\).

lemma (in pmetric_space) gauge_5thCond:

shows \( \mathfrak{B} \subseteq Pow(X\times X) \) using uniform_gauge_def_alt, pmetric_properties(1), func1_1_L3

If the set of positive values is non-empty, then there are sets of the form \(d^{-1}([0,b])\) for \(b>0\).

lemma (in pmetric_space) gauge_6thCond:

assumes \( L_+\neq \emptyset \)

shows \( \mathfrak{B} \neq \emptyset \) using assms, uniform_gauge_def_alt

The remaining 4th condition for the sets of the form \(d^{-1}([0,b])\) to be a uniform base (or a fundamental system of entourages) cannot be proven without additional assumptions in the context of ordered loop valued metrics. To see that consider the example of natural numbers with the metric \(d\langle x,y \rangle = |x-y|\), where we think of \(d\) as valued in the nonnegative set of ordered group of integers. Now take the set \(B_1 = d^{-1}([0,1]) = d^{-1}(\{ 0,1\} )\). Then the set \(B_1 \circ B_1\) is strictly larger than \(B_1\), but there is no smaller set \(B_2\) we can take so that \(B_2 \circ B_2 \subseteq B_1\). One condition that is sufficient is that for every \(b_1 >0\) there is a \(b_2 >0\) such that \(b_2 + b_2 \leq b_1 \). I have not found a standard name for this property, for now we will use the name IsHalfable.

definition

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

The property of halfability written in the notation used in the pmetric_space context.

lemma (in pmetric_space) is_halfable_def_alt:

assumes \( \text{IsHalfable}(L,A,r) \), \( b_1\in L_+ \)

shows \( \exists b_2\in L_+.\ b_2 + b_2 \leq b_1 \) using assms unfolding IsHalfable_def

If the loop order is halfable then for every set \(B_1\) of the form \(d^{-1}([0,b_1])\) for some \(b_1>0\) we can find another one \(B_2 = d^{-1}([0,b_2])\) such that \(B_2\) composed with itself is contained in \(B_1\).

lemma (in pmetric_space) gauge_4thCond:

assumes \( \text{IsHalfable}(L,A,r) \), \( B_1\in \mathfrak{B} \)

shows \( \exists B_2\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1 \)proof
from assms(2) obtain \( b_1 \) where \( b_1\in L_+ \) and \( B_1 = d^{-1}(\{c\in L^+.\ c\leq b_1\}) \) using uniform_gauge_def_alt
from assms(1), \( b_1\in L_+ \) obtain \( b_2 \) where \( b_2\in L_+ \) and \( b_2 + b_2 \leq b_1 \) using is_halfable_def_alt
let \( B_2 = d^{-1}(\{c\in L^+.\ c\leq b_2\}) \)
from \( b_2\in L_+ \) have \( B_2\in \mathfrak{B} \) unfolding UniformGauge_def
{
fix \( p \)
assume \( p \in B_2\circ B_2 \)
with \( B_2\in \mathfrak{B} \) obtain \( x \) \( y \) where \( x\in X \), \( y\in X \) and \( p=\langle x,y\rangle \) using gauge_5thCond
from \( p \in B_2\circ B_2 \), \( p=\langle x,y\rangle \) obtain \( z \) where \( \langle x,z\rangle \in B_2 \) and \( \langle z,y\rangle \in B_2 \) using rel_compdef
with \( B_2\in \mathfrak{B} \) have \( z\in X \) using gauge_5thCond
from \( \langle x,z\rangle \in B_2 \), \( \langle z,y\rangle \in B_2 \) have \( d\langle x,z\rangle + d\langle z,y\rangle \leq b_2 + b_2 \) using pmetric_properties(1), func1_1_L15, add_ineq
with \( b_2 + b_2 \leq b_1 \) have \( d\langle x,z\rangle + d\langle z,y\rangle \leq b_1 \) using loop_ord_trans
with \( x\in X \), \( y\in X \), \( z\in X \), \( p=\langle x,y\rangle \), \( B_1 = d^{-1}(\{c\in L^+.\ c\leq b_1\}) \) have \( p\in B_1 \) using pmetric_properties(4), loop_ord_trans, gauge_members
}
hence \( B_2\circ B_2 \subseteq B_1 \)
with \( B_2\in \mathfrak{B} \) show \( thesis \)
qed

If \(X\) and \(L_+\) are not empty, the order relation \(r\) down-directs \(L_+\), and the loop order is halfable, then \(\mathfrak{B}\) (which in the pmetric_space context is an abbreviation for \(\{ d^{-1}(\{c\in L^+: c\leq b\}: b \in L_+ \}\)) is a fundamental system of entourages, hence its supersets form a uniformity on \(X\) and hence those supersets define a topology on \(X\).

theorem (in pmetric_space) metric_gauge_base:

assumes \( X\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, gauge_1st_cond, gauge_2nd_cond, gauge_3rd_cond, gauge_4thCond, gauge_5thCond, gauge_6thCond, uniformity_base_is_base, uniform_top_is_top unfolding IsUniformityBaseOn_def

At this point we know that a pseudometric induces two topologies: one consisting of unions of open disks (the metric topology) and second one being the uniform topology derived from the uniformity generated the fundamental system of entourages (the base uniformity) of the sets of the form \(d^{-1}([0,b])\) for \(b>0\). The next theorem states that if \(X\) and \(L_+\) are not empty, \(r\) down-directs \(L_+\), and the loop order is halfable, then these two topologies are in fact the same. Recall that in the pmetric_space context \(\tau\) denotes the metric topology.

theorem (in pmetric_space) metric_top_is_uniform_top:

assumes \( X\neq \emptyset \), \( L_+\neq \emptyset \), \( r \text{ down-directs } L_+ \), \( \text{IsHalfable}(L,A,r) \)

shows \( \tau = \text{UniformTopology}( \text{Supersets}(X\times X,\mathfrak{B} ),X) \)proof
let \( \Phi = \text{Supersets}(X\times X,\mathfrak{B} ) \)
from assms have \( \Phi \text{ is a uniformity on } X \) using metric_gauge_base
let \( T = \text{UniformTopology}(\Phi ,X) \)
{
fix \( U \)
assume \( U\in T \)
then have \( U\in Pow(X) \) and I: \( \forall x\in U.\ U\in \{V\{x\}.\ V\in \Phi \} \) unfolding UniformTopology_def
{
fix \( x \)
assume \( x\in U \)
with I obtain \( A \) where \( A\in \Phi \) and \( U = A\{x\} \)
from \( x\in U \), \( U\in T \) have \( x\in \bigcup T \)
with assms have \( x\in X \) using metric_gauge_base(4)
from \( A\in \Phi \) obtain \( B \) where \( B\in \mathfrak{B} \) and \( B\subseteq A \) unfolding Supersets_def
from \( B\in \mathfrak{B} \) obtain \( b \) where \( b\in L_+ \) and \( B = d^{-1}(\{c\in L^+.\ c\leq b\}) \) using uniform_gauge_def_alt
with \( x\in X \), \( B\subseteq A \), \( U = A\{x\} \) have \( disk(x,b) \subseteq U \) using disk_in_gauge(2)
with assms(3), \( x\in X \), \( b\in L_+ \) have \( \exists V\in \tau .\ x\in V \wedge V\subseteq U \) using disks_open, center_in_disk
}
with assms(3) have \( U\in \tau \) using topology0_valid_in_pmetric_space, open_neigh_open
}
thus \( T \subseteq \tau \)
let \( \mathcal{D} = \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)
{
fix \( U \)
assume \( U \in \mathcal{D} \)
then obtain \( c \) \( b \) where \( c\in X \), \( b\in L_+ \), \( U = disk(c,b) \)
{
fix \( x \)
assume \( x\in U \)
let \( b_1 = - d\langle c,x\rangle + b \)
from \( x\in U \), \( c\in X \), \( U = disk(c,b) \) have \( x\in X \), \( x\in disk(c,b) \), \( disk(x,b_1) \subseteq U \), \( b_1 \in L_+ \) using disk_in_disk1, disk_definition, radius_in_loop(4)
with assms(4) obtain \( b_2 \) where \( b_2\in L_+ \) and \( b_2 + b_2 \leq b_1 \) using is_halfable_def_alt
let \( D = \{y\in X.\ d\langle x,y\rangle \leq b_2\} \)
from \( b_2\in L_+ \), \( b_2 + b_2 \leq b_1 \) have \( D \subseteq disk(x,b_1) \) using posset_definition1, positive_subset, add_subtract_pos(3), loop_strict_ord_trans1, disk_radius_strict_mono
let \( B = d^{-1}(\{c\in L^+.\ c\leq b_2\}) \)
from \( b_2\in L_+ \) have \( B\in \mathfrak{B} \) using uniform_gauge_def_alt
then have \( B\in \Phi \) using uniform_gauge_relations, superset_gen
from \( b_2\in L_+ \), \( x\in X \), \( D \subseteq disk(x,b_1) \), \( disk(x,b_1) \subseteq U \) have \( B\{x\} \subseteq U \) using disk_in_gauge(1)
with \( B\in \Phi \) have \( \exists W\in \Phi .\ W\{x\} \subseteq U \)
}
with \( U = disk(c,b) \), \( \Phi \text{ is a uniformity on } X \) have \( U \in T \) using disk_definition, uniftop_def_alt1
}
hence \( \mathcal{D} \subseteq T \)
with assms show \( \tau \subseteq T \) using disks_are_base(1), metric_gauge_base(3), base_smallest_top
qed
end
Definition of IsApseudoMetric: \( \text{IsApseudoMetric}(d,X,G,A,r) \equiv d:X\times X \rightarrow \text{Nonnegative}(G,A,r) \) \( \wedge (\forall x\in X.\ d\langle x,x\rangle = \text{ TheNeutralElement}(G,A))\) \( \wedge (\forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = d\langle y,x\rangle )\) \( \wedge (\forall x\in X.\ \forall y\in X.\ \forall z\in X.\ \langle d\langle x,z\rangle , A\langle d\langle x,y\rangle ,d\langle y,z\rangle \rangle \rangle \in r) \)
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 Nonnegative: \( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
Definition of Disk: \( \text{Disk}(X,d,r,c,R) \equiv \{x\in X.\ \langle d\langle c,x\rangle ,R\rangle \in \text{StrictVersion}(r)\} \)
lemma def_of_strict_ver: shows \( \langle x,y\rangle \in \text{StrictVersion}(r) \longleftrightarrow \langle x,y\rangle \in r \wedge x\neq y \)
Definition of PositiveSet: \( \text{PositiveSet}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)
lemma (in pmetric_space) disk_definition: shows \( disk(c,R) = \{x\in X.\ d\langle c,x\rangle \lt R\} \)
lemma (in loop1) nonneg_definition: shows \( x \in L^+ \longleftrightarrow 0 \leq x \)
lemma (in loop1) loop_strict_ord_trans:

assumes \( x\leq y \) and \( y \lt z \)

shows \( x \lt z \)
lemma (in loop1) posset_definition: shows \( x \in L_+ \longleftrightarrow ( 0 \leq x \wedge x\neq 0 ) \)
lemma (in loop1) ls_other_side:

assumes \( x \lt y \)

shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)
lemma (in pmetric_space) radius_in_loop:

assumes \( c\in X \) and \( x \in disk(c,R) \)

shows \( R\in L \), \( 0 \lt R \), \( R\in L_+ \), \( ( - d\langle c,x\rangle + R) \in L_+ \)
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 \)
lemma (in loop1) nonneg_subset: shows \( L^+ \subseteq L \)
lemma (in loop1) loop_strict_ord_trans1:

assumes \( x \lt y \) and \( y\leq z \)

shows \( x \lt z \)
lemma (in loop1) strict_ord_trans_inv:

assumes \( x \lt y \), \( z\in L \)

shows \( x + z \lt y + z \) and \( z + x \lt z + y \)
lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \)
lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \)
lemma (in loop1) left_right_sub_closed:

assumes \( x\in L \), \( y\in L \)

shows \( ( - x + y) \in L \) and \( x - y \in L \)
lemma (in loop1) loop_ord_refl:

assumes \( x\in L \)

shows \( x\leq x \)
lemma (in pmetric_space) disk_in_disk:

assumes \( c\in X \) and \( x \in disk(c,R) \) and \( m \leq ( - d\langle c,x\rangle + R) \)

shows \( disk(x,m) \subseteq disk(c,R) \)
lemma (in pmetric_space) radius_in_loop:

assumes \( c\in X \) and \( x \in disk(c,R) \)

shows \( R\in L \), \( 0 \lt R \), \( R\in L_+ \), \( ( - d\langle c,x\rangle + R) \in L_+ \)
Definition of DownDirects: \( r \text{ down-directs } X \equiv X\neq 0 \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle z,x\rangle \in r \wedge \langle z,y\rangle \in r) \)
lemma (in pmetric_space) center_in_disk:

assumes \( c\in X \) and \( R\in L_+ \)

shows \( c \in disk(c,R) \)
Definition of SatisfiesBaseCondition: \( B \text{ satisfies the base condition } \equiv \) \( \forall U V.\ ((U\in B \wedge V\in B) \longrightarrow (\forall x \in U\cap V.\ \exists W\in B.\ x\in W \wedge W \subseteq U\cap V)) \)
lemma (in loop1) add_ineq_strict:

assumes \( x \lt y \), \( z \lt t \)

shows \( x + z \lt y + t \)
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 \)
lemma (in loop1) ls_other_side:

assumes \( x \lt y \)

shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)
lemma (in loop1) posset_definition1: shows \( x \in L_+ \longleftrightarrow 0 \lt x \)
lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \)
lemma (in pmetric_space) pmetric_loop_valued:

assumes \( x\in X \), \( y\in X \)

shows \( d\langle x,y\rangle \in L^+ \), \( d\langle x,y\rangle \in L \)
lemma (in pmetric_space) far_disks:

assumes \( x\in X \), \( y\in X \), \( r_x + r_y \leq d\langle x,y\rangle \)

shows \( disk(x,r_x)\cap disk(y,r_y) = \emptyset \)
Definition of MetricTopology: \( \text{MetricTopology}(X,L,A,r,d) \equiv \{\bigcup \mathcal{A} .\ \mathcal{A} \in Pow(\bigcup c\in X.\ \{ \text{Disk}(X,d,r,c,R).\ R\in \text{PositiveSet}(L,A,r)\})\} \)
lemma (in pmetric_space) disks_form_base:

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

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( B \text{ satisfies the base condition } \)
theorem Top_1_2_T1:

assumes \( B \text{ satisfies the base condition } \) and \( T = \{\bigcup A.\ A\in Pow(B)\} \)

shows \( T \text{ is a topology } \) and \( B \text{ is a base for } T \)
lemma (in pmetric_space) metric_top_def_alt:

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( \tau = \{\bigcup A.\ A \in Pow(B)\} \)
theorem (in pmetric_space) disks_are_base:

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

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( B \text{ is a base for } \tau \)
lemma Top_1_2_L5:

assumes \( B \text{ is a base for } T \)

shows \( \bigcup T = \bigcup B \)
theorem (in pmetric_space) pmetric_is_top:

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

shows \( \tau \text{ is a topology } \)
lemma base_sets_open:

assumes \( B \text{ is a base for } T \) and \( U \in B \)

shows \( U \in T \)
theorem (in pmetric_space) disks_are_base:

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

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

shows \( B \text{ is a base for } \tau \)
Definition of IsAmetric: \( \text{IsAmetric}(d,X,G,A,r) \equiv \) \( \text{IsApseudoMetric}(d,X,G,A,r) \wedge (\forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = \text{ TheNeutralElement}(G,A) \longrightarrow x=y) \)
theorem (in pmetric_space) metric_top_carrier:

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

shows \( \bigcup \tau = X \)
lemma (in metric_space) dist_pos:

assumes \( x\in X \), \( y\in X \), \( x\neq y \)

shows \( 0 \lt d\langle x,y\rangle \), \( d\langle x,y\rangle \in L_+ \)
lemma (in loop1) ls_other_side:

assumes \( x \lt y \)

shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)
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 \)
lemma (in pmetric_space) pmetric_loop_valued:

assumes \( x\in X \), \( y\in X \)

shows \( d\langle x,y\rangle \in L^+ \), \( d\langle x,y\rangle \in L \)
lemma (in metric_space) dist_pos:

assumes \( x\in X \), \( y\in X \), \( x\neq y \)

shows \( 0 \lt d\langle x,y\rangle \), \( d\langle x,y\rangle \in L_+ \)
lemma (in loop1) add_subtract_pos:

assumes \( x\in L \), \( 0 \lt y \)

shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \)
lemma (in pmetric_space) disjoint_disks:

assumes \( x\in X \), \( y\in X \), \( r_x \lt d\langle x,y\rangle \)

shows \( ( - r_x + (d\langle x,y\rangle )) \in L_+ \) and \( disk(x,r_x)\cap disk(y, - r_x + (d\langle x,y\rangle )) = 0 \)
lemma exist2_subset:

assumes \( A\subseteq B \) and \( \exists x\in A.\ \exists y\in A.\ \phi (x,y) \)

shows \( \exists x\in B.\ \exists y\in B.\ \phi (x,y) \)
Definition of isT2: \( T \text{ is }T_2 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \) \( (\exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0)) \)
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) uniform_gauge_def_alt: shows \( \mathfrak{B} = \{d^{-1}(\{c\in L^+.\ c\leq b\}).\ b\in L_+\} \)
lemma func1_1_L3:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(D) \subseteq X \)
lemma func1_1_L15:

assumes \( f:X\rightarrow Y \)

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

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

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

assumes \( A\subseteq B \)

shows \( f^{-1}(A) \subseteq f^{-1}(B) \)
Definition of IsAnOrdLoop: \( \text{IsAnOrdLoop}(L,A,r) \equiv \) \( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \) \( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)
Definition of IsPartOrder: \( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)
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 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 \)
lemma (in loop1) loop_zero_nonneg: shows \( 0 \in L^+ \)
lemma symm_vimage_symm:

assumes \( f:X\times X\rightarrow Y \) and \( \forall x\in X.\ \forall y\in X.\ f\langle x,y\rangle = f\langle y,x\rangle \)

shows \( f^{-1}(A) = converse(f^{-1}(A)) \)
lemma (in pmetric_space) gauge_symmetric:

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

shows \( B = converse(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 (in pmetric_space) is_halfable_def_alt:

assumes \( \text{IsHalfable}(L,A,r) \), \( b_1\in L_+ \)

shows \( \exists b_2\in L_+.\ b_2 + b_2 \leq b_1 \)
lemma (in pmetric_space) gauge_5thCond: shows \( \mathfrak{B} \subseteq Pow(X\times X) \)
lemma rel_compdef: shows \( \langle x,z\rangle \in r\circ s \longleftrightarrow (\exists y.\ \langle x,y\rangle \in s \wedge \langle y,z\rangle \in r) \)
lemma (in loop1) add_ineq:

assumes \( x\leq y \), \( z\leq t \)

shows \( x + z \leq y + t \)
lemma (in loop1) loop_ord_trans:

assumes \( x\leq y \) and \( y\leq z \)

shows \( x\leq z \)
lemma (in pmetric_space) gauge_members:

assumes \( x\in X \), \( y\in X \), \( d\langle x,y\rangle \leq b \)

shows \( \langle x,y\rangle \in d^{-1}(\{c\in L^+.\ c\leq b\}) \)
lemma (in pmetric_space) gauge_1st_cond:

assumes \( r \text{ down-directs } L_+ \), \( B_1\in \mathfrak{B} \), \( B_2\in \mathfrak{B} \)

shows \( \exists B_3\in \mathfrak{B} .\ B_3\subseteq B_1\cap B_2 \)
lemma (in pmetric_space) gauge_2nd_cond:

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

shows \( id(X)\subseteq B \)
corollary (in pmetric_space) gauge_3rd_cond:

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

shows \( \exists B_2\in \mathfrak{B} .\ B_2 \subseteq converse(B_1) \)
lemma (in pmetric_space) gauge_4thCond:

assumes \( \text{IsHalfable}(L,A,r) \), \( B_1\in \mathfrak{B} \)

shows \( \exists B_2\in \mathfrak{B} .\ \exists B_2\in \mathfrak{B} .\ B_2\circ B_2 \subseteq B_1 \)
lemma (in pmetric_space) gauge_6thCond:

assumes \( 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 \)
theorem (in pmetric_space) metric_gauge_base:

assumes \( X\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 \)
Definition of UniformTopology: \( \text{UniformTopology}(\Phi ,X) \equiv \{U\in Pow(X).\ \forall x\in U.\ U\in \{V\{x\}.\ V\in \Phi \}\} \)
theorem (in pmetric_space) metric_gauge_base:

assumes \( X\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 \)
Definition of Supersets: \( \text{Supersets}(X,\mathcal{A} ) \equiv \{B\in Pow(X).\ \exists A\in \mathcal{A} .\ A\subseteq B\} \)
lemma (in pmetric_space) disk_in_gauge:

assumes \( b\in L_+ \), \( x\in X \)

defines \( B \equiv d^{-1}(\{c\in L^+.\ c\leq b\}) \)

shows \( B\{x\} = \{y\in X.\ d\langle x,y\rangle \leq b\} \) and \( disk(x,b) \subseteq B\{x\} \)
lemma (in pmetric_space) disks_open:

assumes \( c\in X \), \( R\in L_+ \), \( r \text{ down-directs } L_+ \)

shows \( disk(c,R) \in \tau \)
lemma (in pmetric_space) topology0_valid_in_pmetric_space:

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

shows \( topology0(\tau ) \)
lemma (in topology0) open_neigh_open:

assumes \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)

shows \( V\in T \)
lemma (in pmetric_space) disk_in_disk1:

assumes \( c\in X \) and \( x \in disk(c,R) \)

shows \( disk(x, - d\langle c,x\rangle + R) \subseteq disk(c,R) \)
lemma (in loop1) positive_subset: shows \( L_+ \subseteq L \)
lemma (in loop1) add_subtract_pos:

assumes \( x\in L \), \( 0 \lt y \)

shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \)
lemma (in pmetric_space) disk_radius_strict_mono:

assumes \( r_1 \lt r_2 \)

shows \( \{y\in X.\ d\langle x,y\rangle \leq r_1\} \subseteq disk(x,r_2) \)
lemma superset_gen:

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

shows \( A \in \text{Supersets}(X,\mathcal{A} ) \)
lemma (in pmetric_space) disk_in_gauge:

assumes \( b\in L_+ \), \( x\in X \)

defines \( B \equiv d^{-1}(\{c\in L^+.\ c\leq b\}) \)

shows \( B\{x\} = \{y\in X.\ d\langle x,y\rangle \leq b\} \) and \( disk(x,b) \subseteq B\{x\} \)
lemma uniftop_def_alt1:

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

shows \( \text{UniformTopology}(\Phi ,X) = \{U\in Pow(X).\ \forall x\in U.\ \exists W\in \Phi .\ W\{x\} \subseteq U\} \)
theorem (in pmetric_space) metric_gauge_base:

assumes \( X\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 \)
lemma base_smallest_top:

assumes \( B \text{ is a base for } T \) and \( S \text{ is a topology } \) and \( B\subseteq S \)

shows \( T\subseteq S \)