# Zulip Chat Archive

## Stream: new members

### Topic: Finite Matrix to Finset

#### Jamie Reason (Aug 19 2022 at 09:02):

Is there a way to convert a finite matrix `A : matrix (fin n) (fin n) R`

to a type of `finset R`

? I have a matrix and I want to convert it to a `finset`

, extract an element of that `finset`

, and then say that that must correspond to an element of the matrix. The matrix could have duplicates. So far, I understand it as I have to convert the matrix to a `list`

, then a `multiset`

to not worry about duplicates, then a `finset`

. However, I'm not sure how I'm able to do this.

#### Anne Baanen (Aug 19 2022 at 09:03):

Maybe `finset.image₂`

?

#### Anne Baanen (Aug 19 2022 at 09:04):

More specifically `finset.image₂ A finset.univ finset.univ`

should work.

#### Anne Baanen (Aug 19 2022 at 09:05):

I don't think `finset`

has a specific way to express `image univ`

such as docs#set.range would be (docs#finset.range is the set {0, ..., n-1} instead), so `image`

is probably the most convenient way to go.

#### Jamie Reason (Aug 19 2022 at 09:09):

Thanks very much. If i've used `finset.min'`

for example and have an element `a : R`

, is there a way to say that there must then be some indices with `A i j = a`

?

Last updated: Dec 20 2023 at 11:08 UTC