New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(measure_theory): cleanup and generalize measure' #3648
Conversation
caratheodory_is_measurable -> of_function_caratheodory make the section on caratheodory sets not private generalize more statements about induced_outer_measure
I'm sorry that the diff is not very useful, since I moved lemmas in the process. Perhaps it's helpful to see the diffs before the move: |
also add nolint inhabited for equiv
LGTM modulo 1 comment |
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
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`
Pull request successfully merged into master. Build succeeded: |
There were two functions
measure'
andouter_measure'
with undescriptive names, and which were not very generalrename
measure'
->extend
rename
outer_measure'
->induced_outer_measure
generalize both
extend
andinduced_outer_measure
to an arbitrary subset ofset α
(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 foris_measurable
.Move functions
extend
,induced_outer_measure
andtrim
toouter_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
andouter_measure
The changes in
measurable_space
are almost exclusively style changes.