-
Notifications
You must be signed in to change notification settings - Fork 299
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(order/filter/at_top_bot): use weaker TC assumptions, add lemmas #14105
Conversation
* add `filter.eventually_gt_of_tendsto_at_top`, `filter.eventually_ne_at_bot`, `filter.eventually_lt_of_tendsto_at_bot`; * generalize `filter.eventually_ne_of_tendsto_at_top` and `filter.eventually_ne_of_tendsto_at_bot` from nontrivial ordered (semi)rings to preorders with no maximal/minimal elements.
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.
I use this pattern a lot when working with tendsto
, so I think these lemmas would be very valuable to have
src/order/filter/at_top_bot.lean
Outdated
(eventually_gt_at_top a).mono (λ x hx, hx.ne.symm) | ||
(eventually_gt_at_top a).mono $ λ x, ne_of_gt | ||
|
||
lemma eventually_gt_of_tendsto_at_top [preorder β] [no_max_order β] {f : α → β} {l : filter α} |
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.
I think it would be useful to have the eventually_ge
version of this too
src/order/filter/at_top_bot.lean
Outdated
(eventually_gt_at_top a).mono (λ x hx, hx.ne.symm) | ||
(eventually_gt_at_top a).mono $ λ x, ne_of_gt | ||
|
||
lemma eventually_gt_of_tendsto_at_top [preorder β] [no_max_order β] {f : α → β} {l : filter α} |
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.
Perhaps tendsto.eventually_gt_at_top
to allow dot notation?
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.
Feel free to adopt this PR. I usually use h.eventually (eventually_??_at_top _)
. I've just noticed that we have lemmas that assume [ordered_ring R]
for no reason.
@b-mehta I fixed compile errors. |
Thanks for that @urkud! |
@b-mehta Should we merge it now or wait for a review from one more maintainer? |
I think we should wait for another maintainer to take a look. Perhaps @RemyDegenne? |
LGTM |
…14105) * add `filter.eventually_gt_of_tendsto_at_top`, `filter.eventually_ne_at_bot`, `filter.eventually_lt_of_tendsto_at_bot`; * generalize `filter.eventually_ne_of_tendsto_at_top` and `filter.eventually_ne_of_tendsto_at_bot` from nontrivial ordered (semi)rings to preorders with no maximal/minimal elements. Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Pull request successfully merged into master. Build succeeded: |
add
filter.eventually_gt_of_tendsto_at_top
,filter.eventually_ne_at_bot
,filter.eventually_lt_of_tendsto_at_bot
;generalize
filter.eventually_ne_of_tendsto_at_top
andfilter.eventually_ne_of_tendsto_at_bot
from nontrivial ordered(semi)rings to preorders with no maximal/minimal elements.