Rephrasing a bit:
1. We start with a linearly non-trivial ordered group
$(G,*,<)$, a set $S$ and an application $d:SxS->G$
2. We build the order topology associated to that order .
3. We considered the family of applications $d_x:S->G$ indexed
by $S$; where $d_x(y)=d(x,y)$.
4. We build the initial topology in $S$ associated to the family
of maps ${d_x:S->G| x\in S}$
5 On the other hand we consider the collection of "balls" generated by d.
6. If d satisfies $d(x,y)<= d(y,z)*d(z,x)$ and $d(x,y)=e <->
x=y$ the collection of balls from 5 satisfies the base condition and the generated topology is the same as the one in 4.
I am curious if some kind of reverse of 6 is true. That would tell us why the definition of metric has to be as it is.
Slawek
From: daniel <address@hidden>
To: address@hidden
Sent: Tuesday, September 11, 2012 1:09 PM
Subject: Re: [Isarmathlib-devel] Metric spaces
>Why not a (nontrivial)
linearly ordered group then?
Here is what I think happends:
1. We start with a linearly non-trivial ordered group
$(G,*,<)$, a set $S$ and an application $d:SxS->G$
such that $d(x,y)<= d(y,z)*d(z,x)$ and $d(x,y)=e <->
x=y$.
2. We build the order topology associated to that order (I'll try
to add this example).
3. We considered the family of applications $d_x:S->G$ indexed
by $S$; where $d_x(y)=d(x,y)$.
4. We build the initial topology in $S$ associated to the family
of maps ${d_x:S->G| x\in S}$ (I'll
try to add this example too).
My intuition tells me that this initial topology is the one we get
in the MetricSpace_ZF.thy using a metric
which takes values in an ordered group. This is only an intuition,
I'm not 100% sure.
>If you decide to assume linearly ordered group I suggest you
don't do your development inside the group3
>locale. It uses multiplicative notation which would look
really weird with metric spaces, especially if
>commutativity of the group operation turns out to be needed.
I already did the new development in group4=group3+(linear
order)+(non trivial). Commutativity is not needed.
I suggest to change the name of this construction and reserve the
"Metric Space" notion when in use of a subfield of a model of the
real numbers.
Daniel
PD: I'll upload the new files shortly.
If you decide
to assume linearly ordered group I suggest you don't do your
development inside the group3 locale. It uses multiplicative
notation which would look really weird with metric spaces,
especially if commutativity of the group operation turns out to
be needed.
Slawekk
I considered
you're ideas and I think you're right. Changing the
definition of metric, we can get metric_positive in a
linearly ordered group. This new definition is
equivalent to the previous one in an ordered ring. I'm
not 100% sure, so let me get you back on that in a
couple of days.
I'd be utterly surprised that only a linearly ordered
group is necessary.
Daniel
Daniel,
I
am surprised that it is sufficient to have an
ordered-ring valued metric to get a topology.
Why not a (nontrivial) linearly ordered group
then? I think you can show
metric_positive without using the unit, same with
balls_coverS. Am I missing something?
Slawekk
_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
_______________________________________________
Isarmathlib-devel mailing list
address@hiddenhttps://lists.nongnu.org/mailman/listinfo/isarmathlib-devel