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] - refactor(order/filter/basic): add class filter.ne_bot
#3454
Conversation
This way Lean will find a few most common `≠ ⊥` arguments (incl. `nhds_ne_bot`, `at_top_ne_bot`) automatically.
Docs
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.
You wanted a smaller refactor to relax after the integrals refactor? :-) Thanks for doing this, this is great. I just have two minor comments.
bors d+
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…mathlib into ne-bot-class
bors merge |
I wonder why this isn't batched with #3444. Going to see if I can batch them by hand. |
bors r+ |
This way Lean will f`≠ ⊥` in a few most common cases (incl. `nhds_ne_bot`, `at_top_ne_bot`) automatically. Other API changes: * many lemmas now take `[ne_bot l]` instead of `(hl : l ≠ ⊥)`; * some lemmas got `'` versions that take an explicit `(hl : ne_bot l)`; * rename `ultrafilter_unique` to `is_ultrafilter.unique`; * `cauchy_downwards` is now `cauchy.mono` (instance arg) and `cauchy.mono'` (explicit arg); * `cauchy_map` is now `cauchy.map`; * `cauchy_comap` is now `cauchy.comap`; * `totally_bounded_closure` is now `totally_bounded.closure`; * `totally_bounded_image` is now `totally_bounded.image`;
Pull request successfully merged into master. Build succeeded: |
filter.ne_bot
filter.ne_bot
This way Lean will f
≠ ⊥
in a few most common cases(incl.
nhds_ne_bot
,at_top_ne_bot
) automatically.Other API changes:
[ne_bot l]
instead of(hl : l ≠ ⊥)
;'
versions that take an explicit(hl : ne_bot l)
;ultrafilter_unique
tois_ultrafilter.unique
;cauchy_downwards
is nowcauchy.mono
(instance arg) andcauchy.mono'
(explicit arg);cauchy_map
is nowcauchy.map
;cauchy_comap
is nowcauchy.comap
;totally_bounded_closure
is nowtotally_bounded.closure
;totally_bounded_image
is nowtotally_bounded.image
;