feat(measure_theory): cleanup and generalize measure' (#3648)
There were two functions `measure'` and `outer_measure'` with undescriptive names, and which were not very general
rename `measure'` -> `extend`
rename `outer_measure'` -> `induced_outer_measure`
generalize both `extend` and `induced_outer_measure` to an arbitrary subset of `set α` (instead of just the measurable sets). Most lemmas still hold in full generality, sometimes with a couple more assumptions. For the lemmas that need more assumptions, we have also kept the version that is just for `is_measurable`.
Move functions `extend`, `induced_outer_measure` and `trim` to `outer_measure.lean`.
rename `caratheodory_is_measurable` -> `of_function_caratheodory`
rename `trim_ge` -> `le_trim`
Make the section on caratheodory sets not private (and give a more descriptive name to lemmas).
Style in `measurable_space` and `outer_measure`
