There are really two notions of one-sided real number: lower reals and upper reals. But there is a nearly perfect symmetry between them (although the lower reals seem to get slightly more use).
These are largely concepts in constructive mathematics. Using excluded middle, a bounded one-sided real number is simply a real number, but constructively they are more general (and less well behaved). Lower reals are particularly important in constructive measure theory as the values taken by positive measures (and more generally are used to define extended positive cones).
However, even in classical mathematics, there are some differences, at least in emphasis and application. First, it is most natural to include as a lower real and include as an upper real. (However, you can restrict to bounded lower/upper reals to avoid that, or alternatively genralise to extended lower/upper reals if you want to include both at once.) Also, the natural topology on the lower reals is the lower semicontinuous topology (and the natural topology on the upper reals is the upper semicontinuous topology).
One-sided numbers are sometimes called (upper or lower) semicontinuous numbers. To see why, consider a locale (or topological space) , and consider the (upper or lower) semicontinuous functions (real-valued) on . On the one hand, these are the same as the continuous functions from to (classically) the set of real numbers equipped with the semicontinuous topology or to (constructively) a locale whose points are the one-sided real numbers. On the other hand, these semicontinuous functions are precisely the internal one-sided real numbers in the topos of sheaves over .
Lower and upper reals don't interact well together; for a system that naturally includes both (and, constructively, much more), use the MacNeille real numbers.
(In the following, ‘number’ without qualification may be taken to mean either a real number or a rational number; the result is the same either way. Indeed, we could take any dense set of real numbers.)
A lower real number is the supremum of an inhabited set of numbers. A bounded lower real is the supremum of an inhabited set of numbers that has a finite upper bound. An extended lower real is the supremum of an arbitrary set of numbers.
An upper real number is the infimum of an inhabited set of numbers. A bounded upper real is the infimum of an inhabited set of numbers that has a finite lower bound. An extended lower real is the infimum of an arbitrary set of numbers.
We cannot generalize further by taking more extrema of the same sort. Explicitly, the supremum of any inhabited set of lower reals is a lower real and the infimum of any inhabited set of upper reals is an upper real. (Similar results obtain if we use either bounded or extended reals, so long as we also either require the set to bounded or allow it to be empty.) However, mixing extrema takes us further to the MacNeille real numbers.
There are some choices as to how exactly to represent one-sided real numbers; we will define them here as certain subsets of the set of rational numbers. If we replaced with any other dense subset of the real line, then the definitions would end up being equivalent.
An extended lower real number is any subset of such that
We can actually combine these into a single rule:
A lower real number is an extended lower real such that:
A bounded lower real number is a lower real such that
When treated explicitly as a subset of , we call a lower set. When we interpret as a one-sided real number , we write to mean that . Conversely, we can interpret any rational number, or even any real number, as a bounded lower real, specifically as the set of all rational numbers less than . (A bounded lower real is located if it is the lower real obtained in this way from a real number; classically, every bounded lower real number is located.) We interpret as the lower real whose lower set is all of ; we interpret as the extended lower real whose lower set is empty.
An extended upper real number is any subset of such that
We can actually combine these into a single rule:
An upper real number is an extended upper real such that:
A bounded upper real number is an upper real such that
When treated explicitly as a subset of , we call an upper set. When we interpret as a one-sided real number , we write to mean that . Conversely, we can interpret any rational number, or even any real number, as a bounded upper real, specifically as the set of all rational numbers greater than . (A bounded upper real is located if it is the upper real obtained in this way from a real number; classically, every bounded upper real number is located.) We interpret as the upper real whose upper set is all of ; we interpret as the extended upper real whose upper set is empty.
We define order relations between extended lower reals and as follows:
In other words, is on lower sets, and is (in an appropriate sense).
We define order relations between extended upper reals and as follows:
In other words, is on upper sets, and is .
We now have multiple meanings for or if one or both of these is already a rational number or a real number, but it is a theorem that the meanings are all consistent. We also have for every extended number , and for every bounded number . Finally, if or ; the converse holds classically.
Each version of is a partial order and each version of is a quasiorder. By excluded middle, is a total order and is the corresponding linear order, but neither of these results holds constructively. In particular, the comparison law for is invalid, which is why one-sided reals are not as well behaved as ordinary (located) real numbers.
Given any collection of extended lower reals, their supremum is an extended lower real which is found by taking the union of lower sets. The supremum of an inhabited set of lower reals is a lower real, and the supremum of an inhabited set of bounded lower reals is bounded iff the set has a bounded lower real as an upper bound. In any case, this supremum really is the supremum under . This agrees with the notion of supremum of real numbers in the real number system, when that exists. Every extended lower real is also the supremum in this sense of its corresponding lower set, interpreted as a set of lower reals that happen to all be rational numbers.
Given any collection of extended upper reals, their infimum is an extended upper real which is found by taking the union of upper sets. The infimum of an inhabited set of upper reals is an upper real, and the infimum of an inhabited set of bounded upper reals is bounded iff the set has a bounded upper real as a lower bound. In any case, this infimum really is the infimum under . This agrees with the notion of infimum of real numbers in the real number system, when that exists. Every extended upper real is also the infimum in this sense of its corresponding upper set, interpreted as a set of upper reals that happen to all be rational numbers.
Constructively, we cannot necessarily take the infimum of a set of lower reals, nor the supremum of a set of upper reals. We can, however, interpret such a supremum or infimum as a MacNeille real number.
In general, you can extend order-preserving functions of rational numbers to lower reals and to upper reals; you simply take the image of the lower or upper set and close it downward or upwards, as appropriate. If you have an order-reversing function of rational numbers, then you can apply it to a lower real to get an upper real and conversely; this is about the only interaction that I know of between the two kinds of one-sided real.
Since addition is order-preserving, it works nicely, at least to make a monoid; but subtraction doesn't work in general. Multiplication has trouble with negative numbers but produces good results if you restrict to . Notice that we get with lower reals but with extended upper reals; thus, is a rig for either lower or upper reals, while is a rig only for lower reals. (This doesn't so much mean that upper reals behave worse than lower reals, as that extended reals on either side behave worse.) We can also use logarithms to translate between addition and multiplication. (In particular, with extended lower reals but with extended upper reals.)
Of course, arithmetic with one-sided real numbers is much easier than this in classical mathematics, where the bounded or extended versions may be identified; but even there, the natural operations involving may differ. Accordingly, the conventions for arithmetic with infinities can signal which sort of number is appropriate for a constructive development.
If you really want to do arbitrary arithmetic operations constructively on upper or lower reals, then again you need their common generalisation, the MacNeille reals.
Let's put this on a separate page: semicontinuous topology. For one thing, it's more advanced than the elementary stuff above; for another thing, it's more interesting in classical mathematics; and finally, it's more complicated in constructive mathematics. The main point is that each type of one-sided real number has its own natural topology, and these differ (both classically and constructively) from the usual topology on the real line.
There is a bijective correspondence of internal extended lower real numbers in a sheaf topos of a topological space and lower semicontinuous functions , or equivalently a continuous function , when the latter is equipped with the lower semicontinuous topology. (We will work classically in the external logic.)
Let denote the constant sheaf of rational numbers on . A lower real number in is then defined as a subsheaf of satisfying the axioms above (interpreted in the internal language). Such a lower real number induces a lower semicontinuous function , where denotes the stalk of at (taken as a subset of ).
Conversely, a lower semicontinuous function defines an internal lower real number with sections
over open sets .
See Mulvey (1974, page 28) for details.
For the externally constructive version of this, it is best to take to be a locale; we need to use the (external) locale of lower real numbers in place of , and the notion of semicontinuous map is replaced with a continuous map (in the sense of locales) to .