$title='PRL Formalizing Constructive Real Analysis - Some Theorems'; include_once "../../prlheader.php"; ?>
The surprising thing about the definitions is that they can be thought of in a very intuitive way. For instance, the following lemma says that two real numbers are equal if and only if they have the same limit.
This lemma is useful in showing that real equality is transitive, and thinking
about real equality in terms of limits makes this fact obvious. However, from
the definition alone it seems that transitivity does not hold --- if |a(n)
- b(n)| 2/n and |b(n) - c(n)|
2/n, surely |a(n) -
c(n)| can be made to be greater than 2/n ! The solution is that the
convergence rate in the definition of
prevents this from happening
(the proposed arrangement disqualifies at least one of a, b, and
c from being a real number).
Another characterization of real equality is
which says that if you confuse equal numbers a and b (that is, if you interchange a(i) and b(i) for various i), the resulting sequence is a valid real number.
One fact that was especially useful in proving arithmetic properties is
that any subsequence of a real number is again a real number, equal to the
first. Subsequences are defined by composing a monotone function on
with the real (which is a function
).
There are lemmas about the order relations which provide some more intuition. In particular, a number is nonnegative if and only if its limit is, and positive if and only if there is a 1/n that the sequence stays above from n on (which is a little stricter than saying that the limit is positive).
Now for some more interesting results. For example, the nth element of a real actually approximates the real to within 1/n.
Also, as one might expact, the rationals are dense in the reals.
The following fact is quite important and plays a significant role in the
intermediate value theorem. It is not true in general that a 0
a > 0 for real a, but given an arbitrarily small positive
epsilon we can do almost as well.