Skip to main content
PRL Project



next up previous
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: