Hi!
>I am curious if some kind of reverse of 6 is true.
I don't think there is a reverse of 6, because the balls of
quasipseudometrics also form a base.
Quasi means that "d(x,y)=d(y,x)" doesn't need to hold.
Pseudo means that "d(x,y)=e --> x=y" doesn't need to hold.
The base condition for the balls obtained out of a set $S$, an
ordered group $(G,*,<)$ and a map $d:SxS\to G$ states:
Given $z$ such that $d(x,z)<r1$ and $d(y,z)<r2$ then
exists $a\in S$ and $r3\in G$ where
1.$d(a,z)<r3$
2.$\forall t\in S. d(a,t)<r3 --> d(x,t)<r1
\<and> d(y,t)<r2$
From this I don't see how to extract metric properties out of $d$,
may be you get an idea.
Daniel
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
>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@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
|