Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-05 23:39 a2e76391

View on Github →

feat(order/filter): more eventually/frequently API (#2330)

  • feat(order/filter): more eventually/frequently API
  • Update after review
  • Add simp attribute
  • Update src/order/filter/basic.lean Co-Authored-By: Yury G. Kudryashov urkud@urkud.name
  • Update src/order/filter/basic.lean Co-Authored-By: Yury G. Kudryashov urkud@urkud.name

Estimated changes

added theorem filter.eventually_iff
added theorem filter.eventually_map
added theorem filter.frequently_iff
added theorem filter.frequently_map
added theorem filter.inf_ne_bot_iff