Generalize invertible real functions

[lowasser]

In #1739 -- its current version, at least -- we show that any strictly increasing, (classically) pointwise continuous, unbounded (above and below) function from the real numbers to themselves is an equivalence; the Dedekind reals make this fairly easy.

However, this is substantially more generalizable to any strictly monotonic function between intervals (not necessarily bounded) on the real numbers, and could generalize other functions. Square roots (inverting the square function from the nonnegative reals to themselves) are one example; multiplicative inverses are as well (the multiplicative inverse of x is the inverse function of multiplication by x applied to 1). It may be convenient to express the natural logarithm and inverse trigonometric functions this way as well.

This presumably motivates the definition of arbitrary kinds of interval in the real numbers, though it probably wants one with explicit bound types that include closed, open, and unbounded ends.

There's also no clear answer to how we should name these things. In the draft of #1739, I used the abbreviation SIPCUB rather than repeating "strictly-increasing-pointwise-continuous-unbounded-function" everywhere, and in the absence of a more common name, I think an abbreviation is appropriate, but the naming of the more general version will presumably be even more involved.