-
Notifications
You must be signed in to change notification settings - Fork 298
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] - chore(measure_theory/outer_measure,measure_space): use complete_lattice_of_Inf/Sup
#3185
Conversation
…ice_of_Inf/Sup` Also add a few supporting lemmas about `bsupr`/`binfi` to `order/complete_lattice`
LGTM, but CI failed. Can you restart it? |
I've just restarted it. For future reference (in case it happens again), in the previous run, the |
Ugh, looks like github actions is having troubles again. Let's try restarting it a bit later... |
I tried to run |
Looks good!
|
bors d+ |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…ice_of_Inf/Sup` (#3185) Also add a few supporting lemmas about `bsupr`/`binfi` to `order/complete_lattice`
Pull request successfully merged into master. Build succeeded: |
complete_lattice_of_Inf/Sup
complete_lattice_of_Inf/Sup
…ice_of_Inf/Sup` (leanprover-community#3185) Also add a few supporting lemmas about `bsupr`/`binfi` to `order/complete_lattice`
Also add a few supporting lemmas about
bsupr
/binfi
toorder/complete_lattice