-
Notifications
You must be signed in to change notification settings - Fork 297
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/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable #15307
Conversation
JasonKYi
commented
Jul 13, 2022
I just realized that you don't need the extra lemma because you don't need that the basis is antitone at all, so you could forget the information before applying |
bors r+ |
… which a measurable sequence of functions converges is measurable (#15307) Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Build failed (retrying...): |
bors r- |
Canceled. |
bors r+ |
… which a measurable sequence of functions converges is measurable (#15307) Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Pull request successfully merged into master. Build succeeded: |
… which a measurable sequence of functions converges is measurable (leanprover-community#15307) Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
… which a measurable sequence of functions converges is measurable (#15307) Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
… which a measurable sequence of functions converges is measurable (#15307) Co-authored-by: RemyDegenne <Remydegenne@gmail.com>