Zulip Chat Archive

Stream: Is there code for X?

Topic: Inverse `finset.product`


view this post on Zulip Marcus Rossel (Jan 29 2021 at 17:09):

finset.product takes two finsets and creates a finset of all tuples over them.
Is there an inverse to this? I.e. a function that takes a finset over tuples and splits it into two?

view this post on Zulip Mario Carneiro (Jan 29 2021 at 17:11):

what two?

view this post on Zulip Mario Carneiro (Jan 29 2021 at 17:11):

you could do finset.image prod.fst s

view this post on Zulip Mario Carneiro (Jan 29 2021 at 17:12):

If you want it to be an inverse to finset.product it's not possible though because finset.product s empty = empty so there is no first projection

view this post on Zulip Marcus Rossel (Jan 29 2021 at 17:14):

Mario Carneiro said:

what two?

Say we have {(1, A), (3, B), (3, C), (5, C)} I would want the output to be ({1, 3, 5}, {A, B, C}).

view this post on Zulip Eric Wieser (Jan 29 2021 at 17:14):

I think a better example of Mario's point is that {(1, A), (2, B)} --your_fun--> ({1, 2}, {A, B}) --finset.product--> {(1, A), (2, A), (1, B), (2, B)}

view this post on Zulip Eric Wieser (Jan 29 2021 at 17:15):

So the thing you're looking for cannot be a two-sided inverse

view this post on Zulip Marcus Rossel (Jan 29 2021 at 17:15):

I guess (s.image prod.fst, s.image prod.snd) would work, but it doesn't feel nice.

view this post on Zulip Eric Wieser (Jan 29 2021 at 17:17):

If #5829 goes in and appropriate follow-up PRs made, then that could be changed to be spelt finset.product.symm s, since that's a left-inverse to finset.product edit: that's not true, because finset.product is a function of two arguments, and that PR is about single-argument functions

view this post on Zulip Reid Barton (Jan 29 2021 at 17:20):

Marcus Rossel said:

I guess (s.image prod.fst, s.image prod.snd) would work, but it doesn't feel nice.

I don't understand what's not nice about this

view this post on Zulip Mario Carneiro (Jan 29 2021 at 17:23):

Actually my point is that it can't even be a one-sided inverse because s * empty = empty, so a function f satisfying f (s * t) = s doesn't exist

view this post on Zulip Mario Carneiro (Jan 29 2021 at 17:24):

The reverse inverse definitely doesn't work because not all sets are rectangles


Last updated: May 07 2021 at 22:14 UTC