# Commit 2020-09-22 08:41 b4641efe

View on Github →feat(l1_space): add measurability to integrable (#4170)
This PR defines `integrable`

such that `integrable`

implies `measurable`

. The old version is called `has_finite_integral`

.
This allows us to drop *many* measurability conditions from lemmas that also require integrability.
There are some lemmas that have extra measurability conditions, if it has `integrable`

as conclusion without corresponding `measurable`

hypothesis.
There are many results that require an additional `[measurable_space E]`

hypothesis, and some that require `[borel_space E]`

or `[second_countable_space E]`

(usually when using that addition is measurable).