Functions with compact domain

In this section we concern ourselves with defining operations on the set of functions from an arbitrary interval [a,b] to IR. Although these are a particular kind of partial function, they have the advantage that, given a and b, they have type Set and can thus be quantified over and extracted from existential hypothesis. This will be important when we want to define concepts like differentiability, which involve the existence of an object satisfying some given properties. Throughout this section we will focus on a compact interval and define operators analogous to those we already have for arbitrary partial functions. Let a,b be real numbers and denote by I the compact interval [a,b]. Let f, g be setoid functions of type I → IR.

Constant and identity functions are defined. Let c:IR.

Next, we define addition, algebraic inverse, subtraction and product of functions.

Exponentiation to a natural power n is also useful.

If a function is non-zero in all the interval then we can define its multiplicative inverse.

Absolute value will also be needed at some point.

The set of these functions form a ring with relation to the operations of sum and multiplication. As they actually form a set, this fact can be proved in Coq for this class of functions; unfortunately, due to a problem with the coercions, we are not able to use it (Coq will not recognize the elements of that ring as functions which can be applied to elements of [a,b]), so we merely state this fact here as a curiosity. Finally, we define composition; for this we need two functions with different domains. a',b' be real numbers and denote by I' the compact interval [a',b'], and let g be a setoid function of type I' → IR.