Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-04 09:09 b4a6651f

View on Github →

chore(order/filter/at_top_bot): golf three proofs (#3684) Also add is_countably_generated_at_top.

Estimated changes

Modified src/order/filter/at_top_bot.lean

added theorem filter.at_top_finset_eq_infi

added theorem filter.is_countably_generated_at_top

modified theorem filter.monotone.tendsto_at_top_finset