Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.has_basis.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.has_basis.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.has_basis.small_setsView on Github →