Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-24 17:23 53a484e6

View on Github →

chore(order/filter/small_sets): redefine, golf (#13672) The new definition is defeq to the old one.

Estimated changes

Modified src/order/filter/small_sets.lean

modified def filter.small_sets