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/*): a few lemmas about (is_)measurable
in Π i, π i
#4948
Conversation
urkud
commented
Nov 8, 2020
@@ -350,19 +350,14 @@ iff.refl _ | |||
|
|||
theorem is_measurable_Sup {ms : set (measurable_space α)} {s : set α} : | |||
@is_measurable _ (Sup ms) s ↔ | |||
generate_measurable (⋃₀ (measurable_space.is_measurable' '' ms)) s := | |||
generate_measurable {s : set α | ∃ m ∈ ms, @is_measurable _ m s} s := |
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.
What is the motivation behind this change of statement and the next one?
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.
Both changes were made to avoid using set α → Prop
as set (set α)
. Also I think that the new statements save extra rewrites of mem_sUnion
/mem_Union
both in their proofs, and in lemmas that use them.
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
LGTM bors merge |
Pull request successfully merged into master. Build succeeded: |
(is_)measurable
in Π i, π i
(is_)measurable
in Π i, π i