Finite Matrix to Finset

Stream: new members

[Jamie Reason]

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]

Maybe finset.image₂?

[Anne Baanen]

More specifically finset.image₂ A finset.univ finset.univ should work.

[Anne Baanen]

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]

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?