# Commit 2021-08-12 07:03 cd2b5495

View on Github →chore(measure_theory/*): make measurable_space arguments implicit, determined by the measure argument (#8571) In the measure theory library, most of the definitions that depend on a measure have that form:

```
def example_def {α} [measurable_space α] (μ : measure α) : some_type := sorry
```

Suppose now that we have two `measurable_space`

structures on `α`

: `{m m0 : measurable_space α}`

and we have the measures `μ : measure α`

(which is a measure on `m0`

) and `μm : @measure α m`

. This will be common for probability theory applications. See for example the `conditional_expectation`

file.
Then we can write `example_def μ`

but we cannot write `example_def μm`

because the `measurable_space`

inferred is `m0`

, which does not match the measurable space on which `μm`

is defined. We have to use `@example_def _ m μm`

instead.
This PR implements a simple fix: change `[measurable_space α] (μ : measure α)`

into `{m : measurable_space α} (μ : measure α)`

.
Advantage: we can now use `example_def μm`

since the `measurable_space`

argument is deduced from the `measure`

argument. This removes many `@`

in all places where `measure.trim`

is used.
Downsides:

- I have to write
`(0 : measure α)`

instead of`0`

in some lemmas. - I had to add two
`apply_instance`

to find`borel_space`

instances. - Whenever a lemma takes an explicit measure argument, we have to write
`{m : measurable_space α} (μ : measure α)`

instead of simply`(μ : measure α)`

.