Commit 2020-08-02 04:10 d76c75e9

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