-
Notifications
You must be signed in to change notification settings - Fork 283
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: When the symmetric difference has finite measure #12370
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you rather show that if s ∆ t
has finite measure, then s
has finite measure iff t
has finite measure?
Done! I also added the two implications. |
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…anprover-community/mathlib4 into em/measure_ne_top_of_symmDiff
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Ne.measure_ne_top_of_symmDiff
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Add the following lemma: is `s` and `t` are two measurable sets such that `s` and `s ∆ t` have finite measures, then so does `t`. Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Add the following lemma: is `s` and `t` are two measurable sets such that `s` and `s ∆ t` have finite measures, then so does `t`. Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>
Add the following lemma: is `s` and `t` are two measurable sets such that `s` and `s ∆ t` have finite measures, then so does `t`. Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>
Add the following lemma: is
s
andt
are two measurable sets such thats
ands ∆ t
have finite measures, then so doest
.