Mathlib v3 is deprecated. Go to Mathlib v4

Def filter.small_sets

Modification history

2022-04-24 20:37
src/order/filter/small_sets.lean
refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)
Modified filter.small_setsView on Github →
2022-04-24 17:23
src/order/filter/small_sets.lean
chore(order/filter/small_sets): redefine, golf (#13672) …
Modified filter.small_setsView on Github →
2022-04-22 06:47
src/order/filter/small_sets.lean
feat(order/filter/small_sets): define the filter of small sets (#13467) …
Added filter.small_setsView on Github →