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\).
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)\} \)
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.
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) \)
The next lemma shows the definition of the pseudometric in the notation used in the metric_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_defThe values of the metric are 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 \)proofThe 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\} \)proofIf 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_definitionA technical lemma that allows us to shorten some proofs:
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_+ \)proofIf a point \(x\) is inside a disk \(B\) and \(m\leq R-d(c,x)\) 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) \)proofIf we assume that the order on the group makes the positive set a meet semi-lattice (i.e. every two-element subset of \(G_+\) has a greatest lower bound) then the collection of disks centered at points of the space and with radii in the positive set of the group satisfies the base condition. The meet semi-lattice assumption can be weakened to "each two-element subset of \(G_+\) has a lower bound in \(G_+\)", but we don't do that here.
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 } \)proofDisks 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) = 0 \)proofIf 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 \)proofUnions of disks form a topology, hence (pseudo)metric spaces are topological spaces.
theorem (in pmetric_space) pmetric_is_top:
assumes \( r \text{ down-directs } L_+ \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)
defines \( T \equiv \{\bigcup A.\ A \in Pow(B)\} \)
shows \( T \text{ is a topology } \), \( B \text{ is a base for } T \), \( \bigcup T = X \)proofTo 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_defDistance 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_+ \)proofAn ordered loop valued metric space is \(T_2\) (i.e. Hausdorff).
theorem (in metric_space) metric_space_T2:
assumes \( r \text{ down-directs } L_+ \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)
defines \( T \equiv \{\bigcup A.\ A \in Pow(B)\} \)
shows \( T \text{ is }T_2 \)proofassumes \( x\leq y \) and \( y \lt z \)
shows \( x \lt z \)assumes \( x \lt y \)
shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)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_+ \)assumes \( x \lt y \) and \( y\leq z \)
shows \( x \lt z \)assumes \( x \lt y \), \( z\in L \)
shows \( x + z \lt y + z \) and \( z + x \lt z + y \)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 \)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_+ \)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) \)assumes \( c\in X \) and \( R\in L_+ \)
shows \( c \in disk(c,R) \)assumes \( x \lt y \), \( z \lt t \)
shows \( x + z \lt y + t \)assumes \( x \lt y \)
shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)assumes \( x \lt y \)
shows \( x\in L \) and \( y\in L \)assumes \( x\in X \), \( y\in X \)
shows \( d\langle x,y\rangle \in L^+ \), \( d\langle x,y\rangle \in L \)assumes \( x\in L \)
shows \( x\leq x \)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) = 0 \)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 } \)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 \)assumes \( B \text{ is a base for } T \)
shows \( \bigcup T = \bigcup B \)assumes \( r \text{ down-directs } L_+ \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)
defines \( T \equiv \{\bigcup A.\ A \in Pow(B)\} \)
shows \( T \text{ is a topology } \), \( B \text{ is a base for } T \), \( \bigcup T = X \)assumes \( B \text{ is a base for } T \) and \( U \in B \)
shows \( U \in T \)assumes \( r \text{ down-directs } L_+ \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)
defines \( T \equiv \{\bigcup A.\ A \in Pow(B)\} \)
shows \( T \text{ is a topology } \), \( B \text{ is a base for } T \), \( \bigcup T = X \)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_+ \)assumes \( x \lt y \)
shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)assumes \( x\in X \), \( y\in X \)
shows \( d\langle x,y\rangle \in L^+ \), \( d\langle x,y\rangle \in L \)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_+ \)assumes \( x\in L \), \( 0 \lt y \)
shows \( x - y \lt x \) and \( ( - y + x) \lt x \)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 \)