Ordered finset as list

Stream: Is there code for X?

[Dagur Asgeirsson]

I have a linearly ordered Finset and want it as a List, ordered "correctly". Do we have this? I know of Finset.toList but this doesn't care about the order on J.

import Mathlib.Data.Finset.Basic

variable (I : Type _) [LinearOrder I] (J : Finset I)

/-- J as a list, in the correct order -/
def OrderedFinset.asList : List I := sorry

[Kevin Buzzard]

Can you just now sort it?

[Dagur Asgeirsson]

Ok, I guess this works:

import Mathlib.Data.Finset.Basic
import Mathlib.Data.List.Sort

variable (I : Type _) [LinearOrder I] (J : Finset I)

noncomputable
def OrderedFinset.asList : List I := List.insertionSort (·≤·) J.toList

[Eric Wieser]

docs#Finset.sort

[Eric Wieser]

That one is computable too

[Dagur Asgeirsson]

Cool, thanks!