small sets filter

Stream: maths

[Yury G. Kudryashov]

Hi @Floris van Doorn @Patrick Massot ,
It seems that the recently defined docs#filter.small_sets is the same as l.lift' powerset. We already had some theory about the latter and I used it in measure theory. Do you plan to migrate these uses? Also, if you import order.filter.lift, then you can reuse lemmas like docs#filter.has_basis.lift' instead of proving them once again.

[Yury G. Kudryashov]

I'll do the "import&golf" part now.

[Yury G. Kudryashov]

Done in #13672, moving lemmas from lift to small_sets.

[Yury G. Kudryashov]

Went through git grep 'lift.*powerset' output in #13673

[Patrick Massot]

I forgot that we already had that.

[Yury G. Kudryashov]

Merged master into #13673. Now it's ready for review.

[Floris van Doorn]

Thanks!