Zulip Chat Archive

Stream: maths

Topic: small sets filter


Yury G. Kudryashov (Apr 24 2022 at 15:19):

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 (Apr 24 2022 at 15:55):

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

Yury G. Kudryashov (Apr 24 2022 at 16:11):

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

Yury G. Kudryashov (Apr 24 2022 at 17:12):

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

Patrick Massot (Apr 24 2022 at 17:22):

I forgot that we already had that.

Yury G. Kudryashov (Apr 24 2022 at 19:22):

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

Floris van Doorn (Apr 24 2022 at 22:20):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC