theory MetricSpace_ZF imports Topology_ZF_1 OrderedLoop_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 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 \)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
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 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_+ \)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 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 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
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 \( 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
qed
from assms(2), \( x\in X \), \( m \in L_+ \) have \( W \in B \) and \( x\in W \) using center_in_disk
ultimately show \( thesis \)
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) = 0 \)proof{
}
assume \( disk(x,r_x)\cap disk(y,r_y) \neq 0 \)
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
Unions 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 \)proof from assms 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(2) show \( \bigcup B \subseteq X \) using disk_definition
{
fix \( x \)
assume \( x\in X \)
from assms(1) obtain \( R \) where \( R\in L_+ \) unfolding DownDirects_def
with assms(2), \( x\in X \) have \( x \in \bigcup B \) using center_in_disk
thus \( X \subseteq \bigcup B \)
qed
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_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_+ \)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
An 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 \)proof{
}
fix \( x \) \( y \)
assume \( x\in \bigcup T \), \( y\in \bigcup T \), \( x\neq y \)
from assms have \( B\subseteq T \) using pmetric_is_top(2), base_sets_open
moreover
have \( \exists U\in B.\ \exists V\in B.\ x\in U \wedge y\in V \wedge U\cap V = 0 \)proof
}
ultimately have \( \exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V = 0 \)
let \( R = d\langle x,y\rangle \)
from assms have \( \bigcup T = X \) using pmetric_is_top(3)
with \( x\in \bigcup T \), \( y\in \bigcup T \) have \( x\in X \), \( y\in X \)
with \( x\neq y \) have \( R\in L_+ \) using dist_pos
with assms(2), \( 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) = 0 \)
moreover
from assms(2), \( 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 {
}
ultimately show \( thesis \)
qed
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), 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 assms(2), \( 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 \)
then show \( thesis \) unfolding isT2_def
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 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) 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 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 loop1) loop_ord_refl:
assumes \( x\in L \)
shows \( x\leq x \) 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 \) 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 Top_1_2_L5:
assumes \( B \text{ is a base for } T \)
shows \( \bigcup T = \bigcup B \)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) 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 \) lemma base_sets_open:
assumes \( B \text{ is a base for } T \) and \( U \in B \)
shows \( U \in T \) 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 \) 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) subtract_pos:
assumes \( x\in L \), \( 0 \lt y \)
shows \( x - y \lt x \) and \( ( - y + x) \lt 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 \)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)) \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8