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