Description: A characterization of measurability in terms of simple functions (this
is an if and only if for nonnegative functions, although we don't prove
it). Any nonnegative measurable function is the limit of an increasing
sequence of nonnegative simple functions. This proof is an example of a
poor de Bruijn factor - the formalized proof is much longer than an
average hand proof, which usually just describes the function G and
"leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014)(Revised by Mario Carneiro, 23-Aug-2014)