|
From: | daniel |
Subject: | Re: [Isarmathlib-devel] Metric spaces |
Date: | Tue, 11 Sep 2012 13:09:00 +0200 |
User-agent: | Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:15.0) Gecko/20120907 Thunderbird/15.0.1 |
>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.
|
[Prev in Thread] | Current Thread | [Next in Thread] |