## Stream: Is there code for X?

### Topic: Inverse finset.product

#### 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?

what two?

#### Mario Carneiro (Jan 29 2021 at 17:11):

you could do finset.image prod.fst s

#### 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

#### 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}).

#### 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)}

#### Eric Wieser (Jan 29 2021 at 17:15):

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

#### 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.

#### 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

#### 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.

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