# 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: May 07 2021 at 22:14 UTC