Re: Midpoint in the waters between Scylla and Charybdis...
> Date: Thu, 08 Mar 2012 22:41:37 -0500
> To: stds-1788 <stds-1788@xxxxxxxxxxxxxxxxx>
> From: Michel Hack <mhack@xxxxxxx>
> Subject: Midpoint in the waters between Scylla and Charybdis...
>
> Dan Zuras wrote:
> > X \subset Y ==> if (inf(X)==inf(Y)) then mid(X) <= mid(Y)
> > X \subset Y ==> if (sup(X)==sup(Y)) then mid(X) >= mid(Y)
> >
> > ... The last 2 for well ordering.
>
> Well-ordering of what? Please note that at Level 1 the natural order
> of the Reals is not a well-order (though it is at Level 2, because of
> the next_up() function -- and really because the Level 2 set is finite).
>
> Did you (Dan) mean "total ordering" of inf <= mid <= sup perhaps?
>
> Michel.
> ---Sent: 2012-03-09 03:48:47 UTC
It has been a long time since we discussed it in light
of the other controversies.
It is simple, really. If two intervals X & Y are
coincident at one end, they are weakly ordered by
midpoint in the same sense as their containment order.
Not difficult, really. But the truth of it depends on
weakly ordered arithmetic as much as a careful definition
of midpoint.
And it might be useful in proofs.
That's all.
Dan