## Stream: new members

### Topic: How to convert finset N to list N

#### Rui Liu (Dec 09 2020 at 23:20):

Given s: finset N, I want to get a list of sorted values, how do I do that? I tried s.sort nat.lt but that doesn't work.

#### Adam Topaz (Dec 09 2020 at 23:20):

I think there's a docs#finset.to_list ?

#### Eric Wieser (Dec 09 2020 at 23:21):

I think it was more an exists_list

#### Kevin Buzzard (Dec 09 2020 at 23:21):

There's docs#finset.sort

#### Adam Topaz (Dec 09 2020 at 23:23):

I guess F.1.1 or something like that should spit out some list

#### Rob Lewis (Dec 09 2020 at 23:23):

You need to sort by a total relation, try nat.le. Best written as

import data.finset
example (s : finset ℕ) : list ℕ := s.sort (≤)


#### Adam Topaz (Dec 09 2020 at 23:23):

where F is a finset

#### Rui Liu (Dec 09 2020 at 23:24):

Oh shit, nat.le works whereas nat.lt doesn't work? Why is that so?

#### Kevin Buzzard (Dec 09 2020 at 23:24):

If you look at the docs it says it wants a total order

#### Adam Topaz (Dec 09 2020 at 23:25):

There's also a docs#multiset.to_list so you can do F.1.to_list

#### Kevin Buzzard (Dec 09 2020 at 23:25):

you can just click through to see the definitions. is_total means docs#is_total which is true for \le but not \lt

#### Rui Liu (Dec 09 2020 at 23:26):

Oh, since we don't have x < x in both direction, < is not a total order, whereas <= is!

Thanks!

Right

#### Adam Topaz (Dec 09 2020 at 23:28):

(Oh, I just read that you wanted it sorted, sorry! If you don't care about sorting for some reason, you can convert to a multiset then to a list.)

Last updated: Dec 20 2023 at 11:08 UTC