isarmathlib-devel
[Top][All Lists]
Advanced
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Isarmathlib-devel] Metric spaces

From: daniel
Subject: Re: [Isarmathlib-devel] Metric spaces
Date: Mon, 10 Sep 2012 22:23:42 +0200
User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:15.0) Gecko/20120824 Thunderbird/15.0
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

reply via email to
[Prev in Thread] Current Thread [Next in Thread]