Zulip Chat Archive

Stream: Is there code for X?

Topic: filter.eventually_pi

Yaël Dillies (Mar 22 2023 at 01:59):

We have docs#filter.eventually.prod_mk for the interaction between docs#filter.eventually and docs#filter.prod. Where is the analogous lemma for docs#filter.pi?

Anatole Dedecker (Mar 22 2023 at 14:50):

I think it’s not true, because you can’t swap the usual forall and docs#filter.eventually

Anatole Dedecker (Mar 22 2023 at 14:50):

Or at least the statement would need to be more complicated

Reid Barton (Mar 22 2023 at 14:57):

Maybe the assumption is that the indexing set of the pi is finite.

Yaël Dillies (Mar 22 2023 at 15:36):

Yes, I am happy with a finite indexing type. I don't know the correct generality but I was surprised that we have no version of it at all.

Anatole Dedecker (Mar 22 2023 at 20:13):

Oh right if the indexing set is finite then it is definitely true. It seems that we indeed lack some API for this case, but docs#filter.eventually_all should allow you to emulate the proof of the binary case

Yaël Dillies (Mar 23 2023 at 11:17):

Thanks for the hint! It's now in #18629.

Last updated: Dec 20 2023 at 11:08 UTC