Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.small_sets_eq_generate

Modification history

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_sets_eq_generateView on Github →