IsarMathLib

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

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

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

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

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

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.

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

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

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

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

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.

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

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

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

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.

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

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

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

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.

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

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

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

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

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

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

Distance of different points is greater than zero.

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

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

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

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

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

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

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

Gauges corresponding to larger elements of the loop are larger.

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

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

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

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

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

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

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.

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

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

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

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.