Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-04 08:09 d88042c1

View on Github →

feat(order/filter/at_top_bot): lemmas about map/comap of at_top/at_bot (#4878)

  • Redefine at_top/at_bot using Ici/Iic.
  • Add lemmas about map/comap of at_top/at_bot under coe : s → α, where s is one of Ici a, Iic a, Ioi a, Iio a.

Estimated changes

modified def filter.at_bot
added theorem filter.at_bot_Iic_eq
added theorem filter.at_bot_Iio_eq
modified def filter.at_top
added theorem filter.at_top_Ici_eq
added theorem filter.at_top_Ioi_eq