Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-09 21:17 ac62213b

View on Github →

chore(order/filter/at_top_bot): in order_top at_top = pure ⊤ (#3346)

Estimated changes

Modified src/order/filter/at_top_bot.lean

added theorem filter.order_top.at_top_eq

added theorem filter.tendsto_at_top_pure

Modified src/topology/basic.lean

added theorem order_top.tendsto_at_top