Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-05 07:50 39a3b58b

View on Github →

feat(order/filter/at_top_bot): order_iso maps at_top to at_top (#5236)

Estimated changes

Modified src/order/filter/at_top_bot.lean

added theorem order_iso.comap_at_bot

added theorem order_iso.comap_at_top

added theorem order_iso.map_at_bot

added theorem order_iso.map_at_top

added theorem order_iso.tendsto_at_bot

added theorem order_iso.tendsto_at_bot_iff

added theorem order_iso.tendsto_at_top

added theorem order_iso.tendsto_at_top_iff