theory MetricSpace_ZF imports Topology_ZF_1 OrderedGroup_ZF Lattice_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 group.
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 group carrier \(G\), the group 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 use additive notation for the group operation but we do not assume that the group is abelian. Since for many theorems it is sufficient to assume the pseudometric axioms we will assume in this context that the sets \(d,X,G,A,r\) form a pseudometric raher than a metric.
Locale pmetric_space
assumes ordGroupAssum: \( \text{IsAnOrdGroup}(G,A,r) \)
assumes pmetricAssum: \( \text{IsApseudoMetric}(d,X,G,A,r) \)
defines \( 0 \equiv \text{TheNeutralElement}(G,A) \)
defines \( x + y \equiv A\langle x,y\rangle \)
defines \( ( - x) \equiv \text{GroupInv}(G,A)(x) \)
defines \( x \leq y \equiv \langle x,y\rangle \in r \)
defines \( x \lt y \equiv x\leq y \wedge x\neq y \)
defines \( G^+ \equiv \text{Nonnegative}(G,A,r) \)
defines \( G_+ \equiv \text{PositiveSet}(G,A,r) \)
defines \( -C \equiv \text{GroupInv}(G,A)(C) \)
defines \( abs(x) \equiv \text{AbsoluteValue}(G,A,r)(x) \)
defines \( f^\circ \equiv \text{OddExtension}(G,A,r,f) \)
defines \( disk(c,R) \equiv \text{Disk}(X,d,r,c,R) \)
The theorems proven the in the group3 locale are valid in the pmetric_space locale.
Sublocale pmetric_space < group3
using ordGroupAssum unfolding group3_def
The theorems proven the in the group0 locale are valid in the pmetric_space locale.
Sublocale pmetric_space < group0
using ordGroupAssum unfolding group0_def , IsAnOrdGroup_def
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 G^+ \), \( \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 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
qed
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 \)
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 G_+ \)
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_group:
assumes \( c\in X \) and \( x \in disk(c,R) \)
shows \( R\in G \), \( 0 \lt R \), \( R\in G_+ \), \( (( - d\langle c,x\rangle ) + R) \in G_+ \)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 , OrderedGroup_ZF_1_L2 , group_strict_ord_transit
then show \( R\in G \) and \( R\in G_+ \) using OrderedGroup_ZF_1_L2A , less_are_members
from assms(1), \( x\in X \) have \( d\langle c,x\rangle \in G \) using pmetric_properties(1) , apply_funtype , OrderedGroup_ZF_1_L4E
then have \( ( - d\langle c,x\rangle ) \in G \) using inverse_in_group
with \( R\in G \), \( d\langle c,x\rangle \lt R \) have \( ( - d\langle c,x\rangle ) + d\langle c,x\rangle \lt ( - d\langle c,x\rangle ) + R \) using group_strict_ord_transl_inv(2)
with \( d\langle c,x\rangle \in G \) show \( (( - d\langle c,x\rangle ) + R) \in G_+ \) using group0_2_L6 , OrderedGroup_ZF_1_L2A , less_are_members
qed
If 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) \)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 G \), \( x\in X \), \( y\in X \) using radius_in_group(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 G \) using pmetric_properties(1) , apply_funtype , OrderedGroup_ZF_1_L4E
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 OrderedGroup_ZF_1_L4A , group_strict_ord_transl_inv(2)
with \( d\langle c,x\rangle \in G \), \( R\in G \), \( 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 inv_cancel_two(4) , group_strict_ord_transit , disk_definition
qed
If 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 \( \text{IsMeetSemilattice}(G_+,r \cap G_+\times G_+) \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in G_+\} \)
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 G_+ \), \( c_V \in X \), \( R_V \in G_+ \), \( 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 G_+ \) and \( m_V\in G_+ \) using radius_in_group(4)
let \( m = \text{Meet}(G_+,r \cap G_+\times G_+)\langle m_U,m_V\rangle \)
let \( W = disk(x,m) \)
from assms(1), \( m_U \in G_+ \), \( m_V \in G_+ \) have \( \langle m,m_U\rangle \in r \cap G_+\times G_+ \) using meet_val(3)
moreover
from assms(1), \( m_U \in G_+ \), \( m_V \in G_+ \) have \( \langle m,m_V\rangle \in r \cap G_+\times G_+ \) using meet_val(4)
moreover from assms(1), \( m_U \in G_+ \), \( m_V \in G_+ \) have \( m \in G_+ \) using meet_val(1)
ultimately have \( m \in G_+ \), \( m \leq m_U \), \( m \leq m_V \)
with \( 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
qed
from assms(2), \( x\in X \), \( m \in G_+ \) have \( W \in B \) and \( x\in W \) using center_in_disk
ultimately show \( thesis \)
then show \( thesis \) unfolding SatisfiesBaseCondition_def
qed
Unions of disks form a topology, hence (pseudo)metric spaces are topological spaces. We have to add the assumption that the positive set is not empty. This is necessary to show that we can cover the space with disks and it does not look like it follows from anything we have assumed so far.
theorem (in pmetric_space) pmetric_is_top:
assumes \( \text{IsMeetSemilattice}(G_+,r \cap G_+\times G_+) \), \( G_+\neq 0 \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in G_+\} \)
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 \)proof from assms(1,3,4) show \( T \text{ is a topology } \), \( B \text{ is a base for } T \) using disks_form_base , Top_1_2_T1
then have \( \bigcup T = \bigcup B \) using Top_1_2_L5
moreover
qed
have \( \bigcup B = X \)proof
}
ultimately show \( \bigcup T = X \)
from assms(3) show \( \bigcup B \subseteq X \) using disk_definition
{
fix \( x \)
assume \( x\in X \)
from assms(2) obtain \( R \) where \( R\in G_+ \)
with assms(3), \( x\in X \) have \( x \in \bigcup B \) using center_in_disk
thus \( X \subseteq \bigcup B \)
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) \)
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}(G,P,r) \equiv \)
\( \{x\in G.\ \langle \text{TheNeutralElement}(G,P),x\rangle \in r \wedge \text{TheNeutralElement}(G,P)\neq x\} \)
lemma (in pmetric_space) disk_definition: shows \( disk(c,R) = \{x\in X.\ d\langle c,x\rangle \lt R\} \)
lemma (in pmetric_space) pmetric_properties: shows \( d: X\times X \rightarrow G^+ \), \( \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 group3) OrderedGroup_ZF_1_L2: shows \( g\in G^+ \longleftrightarrow 1 \leq g \)
lemma (in group3) group_strict_ord_transit:
assumes \( a\leq b \) and \( b \lt c \)
shows \( a \lt c \) lemma (in group3) OrderedGroup_ZF_1_L2A: shows \( g\in G_+ \longleftrightarrow (1 \leq g \wedge g\neq 1 ) \)
lemma (in group3) less_are_members:
assumes \( a \lt b \)
shows \( a\in G \), \( b\in G \) lemma (in group3) OrderedGroup_ZF_1_L4E: shows \( G^+ \subseteq G \)
lemma (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\in G \) lemma (in group3) group_strict_ord_transl_inv:
assumes \( a \lt b \) and \( c\in G \)
shows \( a\cdot c \lt b\cdot c \), \( c\cdot a \lt c\cdot b \) lemma (in group0) group0_2_L6:
assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \) lemma (in pmetric_space) radius_in_group:
assumes \( c\in X \) and \( x \in disk(c,R) \)
shows \( R\in G \), \( 0 \lt R \), \( R\in G_+ \), \( (( - d\langle c,x\rangle ) + R) \in G_+ \) lemma (in pmetric_space) pmetric_properties: shows \( d: X\times X \rightarrow G^+ \), \( \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 group3) OrderedGroup_ZF_1_L4A:
assumes \( a \lt b \) and \( b\leq c \)
shows \( a \lt c \) lemma (in group0) inv_cancel_two:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \) lemma (in pmetric_space) radius_in_group:
assumes \( c\in X \) and \( x \in disk(c,R) \)
shows \( R\in G \), \( 0 \lt R \), \( R\in G_+ \), \( (( - d\langle c,x\rangle ) + R) \in G_+ \) lemma meet_val:
assumes \( \text{IsMeetSemilattice}(L,r) \), \( x\in L \), \( y\in L \)
defines \( m \equiv \text{Meet}(L,r)\langle x,y\rangle \)
shows \( m\in L \), \( m = \text{Infimum}(r,\{x,y\}) \), \( \langle m,x\rangle \in r \), \( \langle m,y\rangle \in r \) lemma meet_val:
assumes \( \text{IsMeetSemilattice}(L,r) \), \( x\in L \), \( y\in L \)
defines \( m \equiv \text{Meet}(L,r)\langle x,y\rangle \)
shows \( m\in L \), \( m = \text{Infimum}(r,\{x,y\}) \), \( \langle m,x\rangle \in r \), \( \langle m,y\rangle \in r \) lemma meet_val:
assumes \( \text{IsMeetSemilattice}(L,r) \), \( x\in L \), \( y\in L \)
defines \( m \equiv \text{Meet}(L,r)\langle x,y\rangle \)
shows \( m\in L \), \( m = \text{Infimum}(r,\{x,y\}) \), \( \langle m,x\rangle \in r \), \( \langle m,y\rangle \in r \) 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) center_in_disk:
assumes \( c\in X \) and \( R\in G_+ \)
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 pmetric_space) disks_form_base:
assumes \( \text{IsMeetSemilattice}(G_+,r \cap G_+\times G_+) \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in G_+\} \)
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 Top_1_2_L5:
assumes \( B \text{ is a base for } T \)
shows \( \bigcup T = \bigcup B \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8