# Zulip Chat Archive

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

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

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 ~~ edit: that's not true, because finset.product is a function of two arguments, and that PR is about single-argument functions`finset.product.symm s`

, since that's a left-inverse to `finset.product`

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

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

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