Re: [Isarmathlib-devel] Metric spaces

[Slawomir Kolodynski]

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

---

From: daniel <address@hidden>
To: address@hidden
Sent: Monday, September 10, 2012 10:23 PM
Subject: Re: [Isarmathlib-devel] Metric spaces

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