Re: [mizar] How to search for a lemma?

[Freek Wiedijk <freek@cs.kun.nl>]

Bob:

>It's also true that every complete ordered field is Archimedian.
>{If not, the set of integers has an upper bound, hence a least upper
>bound, say x. But then, easily, x -1 is also an upper bound of Int,
>contradicting leastness.}

That's interesting, as we have Archimedian-ness as a separate
property in our structures, I think.

But we have stated completeness as the property that every
Cauchy sequence has a limit (I think: just the existence of
the limit, not uniqueness) and not that every set that has an
upper bound has a supremum.  So can you also get
Archimedian-ness from that?

For the record, our Cauchy sequences are not defined as "for
k ex N st ... < 1/k", but as "for eps st eps > 0 ex N st
... < eps".

I would expect that maybe the "non-standard reals" should be
complete in our sense, but that they are not Archimedian with
respect to the standard natural numbers.

Freek