Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-02 22:16 5c3606dd

View on Github →

feat(order/filter/basic): define filter.eventually and filter.frequently (#1845)

  • feat(order/filter/basic): define filter.eventually and filter.frequently As suggested in #119
  • More lemmas, use notation
  • Fix a typo
  • Update src/order/filter/basic.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/order/filter/basic.lean
  • Add a short file docstring
  • Update src/order/filter/basic.lean

Estimated changes

added theorem filter.eventually.mono
added theorem filter.eventually.mp
added theorem filter.eventually_true
added theorem filter.frequently.mono
added theorem filter.frequently.mp