Set over Fintype to List

Stream: Is there code for X?

[Martin Dvořák]

example {T : Type} [Fintype T] (s : Set T) :
  ∃ l : List T, ∀ t : T, t ∈ s ↔ t ∈ l := sorry

ideally as something executable

[Anne Baanen]

Without an order on T, you could extract the List underlying the Multiset of docs#Fintype.univ. There is an executable (but not sound) version where it looks through the quotient type.

[Anne Baanen]

Otherwise you need a linear order on T and then you can use docs#Finset.sort.

[Yakov Pechersky]

Because it's fintype, and you only need to prove existence, not construction, you can also choose an arbitrary perm to Fin, and use that to either define an arbitrary order on the type, so that you can use Finset.sort. But I think, like Anne said, choosing an arbitrary list representation of Finset.univ and then applying List.filter on it should be enough.

[Eric Wieser]

Can you un-#xy? If you want this list computably, probably you should be using Quotient.lift or similar instead