**Next:**Some Theorems

**Up:**Real Analysis in

**Previous:**Definitions

## Well-Formedness and Functionality

Since is a proper subset of ` Seq( )` it is necessary to
prove that the operations above actually produce real numbers. In Nuprl such
``well-formedness'' proofs are generally required and usually trivial. With the
constructive reals, though, these proofs are anything but
routine, and in fact are the reason that the definitions are so complicated.
Thus the following theorems deserve to be mentioned:

Another concern is that functions are well defined with respect to real
equality. That is, they do not depend on the
particular sequences representing their arguments. For example, the canonical
bound of a number is * not* functional.

This theorem is not quite as trivial as it looks --- the equality on the left is rational equality whereas the one on the right is real equality.

Similarly the order relations are well defined: