set to finset equiv

Stream: Is there code for X?

[Yakov Pechersky]

Something akin to

noncomputable def classicize {α : Type*} [decidable_eq α] [fintype α] : set α ≃ finset α := sorry

[Eric Rodriguez]

doesn't seem too hard to prove using set.to_finset if it's not around

[Eric Rodriguez]

although funnily enough my computer won't find an instance of fintype ↥s from fintype α

[Eric Wieser]

You need decidability for that, Eric

[Eric Rodriguez]

decidable_pred s?

[Eric Wieser]

decidable_pred (\mem s)

[Eric Rodriguez]

@[simp] lemma finset.to_finset_coe {α : Type*} (s : finset α) : set.to_finset (s : set α) = s :=
by rw set.to_finset; ext; simp

noncomputable def classicize {α : Type*} [decidable_eq α] [fintype α] : set α ≃ finset α :=
{ to_fun := λ s, by {classical; exact set.to_finset s},
  inv_fun := λ s, s,
  left_inv := λ x, by simp,
  right_inv := λ x, by { dsimp only, convert finset.to_finset_coe x } }

[Eric Rodriguez]

terrible code but it will work

[Eric Wieser]

Do we have docs#set.to_finset_coe?

[Eric Rodriguez]

we have the set = set version, finset = finset isn't there

[Eric Wieser]

What's that one called?

[Eric Rodriguez]

docs#set.coe_to_finset

[Eric Rodriguez]

edited to something slightly less terrible, but it's not quite as clean as it should be due to different fintype instances, same thing as earlier today lol

[Eric Rodriguez]

maybe that's why it's not been put in yet

[Kevin Buzzard]

There should be a map from set to finset sending infinite sets to zero