Commit 2022-05-16 13:42 a9e74ab7
View on Github →feat(order/filter/at_top_bot): use weaker TC assumptions, add lemmas (#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
andfilter.eventually_ne_of_tendsto_at_bot
from nontrivial ordered (semi)rings to preorders with no maximal/minimal elements.