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