Inverting monotone continuous functions in constructive analysis

Abstract

We prove constructively (in the style of Bishop) that every monotone continuous function with a uniform modulus of increase has a continuous inverse. The proof is formalized, and a realizing term extracted. This term can be applied to concrete continuous functions and arguments, and then normalized to a rational approximation of say a zero of a given function, It turns out that even in the logical term language "normalization by evaluation" is reasonably efficient. © Springer-Verlag Berlin Heidelberg 2006.