Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 01:46 95852107

View on Github →

chore(order/filter): add a few lemmas (#4661)

Estimated changes

Modified src/order/filter/at_top_bot.lean

added theorem filter.at_top_basis_Ioi

added theorem filter.eventually_gt_at_top

added theorem filter.eventually_lt_at_bot

Modified src/order/filter/bases.lean

added theorem filter.has_basis.frequently_iff

Modified src/order/filter/basic.lean

modified theorem filter.eventually_sup

added theorem filter.tendsto_top