Zulip Chat Archive

Stream: Is there code for X?

Topic: Sorted set


Sebastien Gouezel (Mar 01 2020 at 09:00):

Assume I have a subset of fin n of cardinality k. I would like to get the increasing map fin k -> fin n that parameterizes it. Is it already in mathlib? Otherwise, my approach would be first to do it for infinite subsets of (to avoid dealing with emptiness issues and option), and then reduce to this case by extending my subset of fin n to a subset of by filling on the right, and then taking the first k elements of the resulting parameterization on . But I guess some people might complain that this approach does not compute well...

Mario Carneiro (Mar 01 2020 at 10:06):

You can sort a finset, and then use nth to get the elements in numeric order. There is a bit of plumbing to make the domain fin k specifically but not too much, especially if computation doesn't matter


Last updated: Dec 20 2023 at 11:08 UTC