Description: A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016)