mathlib3

34613996 - refactor(integration.lean): changing `measure_space` to `measurable_space` (#1072)

refactor(integration.lean): changing `measure_space` to `measurable_space` (#1072) I've been using this file and `range_const` doesn't seem to require the spurious `measure_space` instance. `measurable_space` seems to suffice.