Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.has_antitone_basis.tendsto

Modification history

2022-05-07 07:07
src/order/filter/at_top_bot.lean
feat(order/filter): add a few lemmas (#13985) …
Deleted filter.has_antitone_basis.tendstoView on Github →
2021-09-27 10:29
src/order/filter/at_top_bot.lean
chore(order): globally replace "antimono" with "antitone" (#9400) …
Added filter.has_antitone_basis.tendstoView on Github →