Sorted set

Stream: Is there code for X?

[Sebastien Gouezel]

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]

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