finset α ≃ set α

Stream: Is there code for X?

[Violeta Hernández]

Do we have the equivalence finset α ≃ set α for fintype α?

[Violeta Hernández]

Similarly for α →₀ β and α → β

[Adam Topaz]

The one for finsupp is definitely there... I don't know about the finset one, but certainly all the simp lemmas are around, e.g.

import data.set.finite

noncomputable
example {α : Type*} [fintype α] : finset α ≃ set α :=
{ to_fun := λ A, A,
  inv_fun := λ A, (set.finite.of_fintype A).to_finset,
  left_inv := λ A, by simp only [finset.finite_to_set_to_finset],
  right_inv := λ A, by simp only [set.finite.coe_to_finset]}

[Adam Topaz]

docs#finsupp.equiv_fun_on_fintype

[Kyle Miller]

The "right" way to go from a set to a finset is docs#set.to_finset though it needs a number of decidability assumptions to work (not that this equivalence could ever be computable -- you'd need some bundled set that included a decidable_pred instance for the membership test).

import data.set.finite

noncomputable
example {α : Type*} [fintype α] : finset α ≃ set α :=
{ to_fun := coe,
  inv_fun := by classical; exact λ A, A.to_finset,
  left_inv := λ A, by { ext, rw [set.mem_to_finset, finset.mem_coe] },
  right_inv := λ A, by rw [set.coe_to_finset] }

[Adam Topaz]

Thhis works

import data.set.finite

example {α : Type*} [fintype α] [∀ (S : set α) t, decidable (t ∈ S)] : finset α ≃ set α :=
{ to_fun := λ A, A,
  inv_fun := λ A, A.to_finset,
  left_inv := λ A, by { ext, dsimp, simp },
  right_inv := λ A, by simp }

[Adam Topaz]

The ext, dsimp, simp dance probably means we're missing a lemma there..

[Kyle Miller]

[∀ (S : set α) t, decidable (t ∈ S)] is an extremely strong assumption, though. If α has cardinality at least two I'm pretty sure it's equivalent to [∀ p, decidable p].

[Adam Topaz]

Fair enough... I'll go back to my classical cave where I can actually choose stuff.

[Yaël Dillies]

Yes, you can embed any proposition into set α for a nontrivial α.

[Junyan Xu]

Not necessarily nontrivial/card at least two:

example (h : Π (S : set unit) t, decidable (t ∈ S)) (p) : decidable p :=
begin
  cases h {x | p} () with hp hp,
  exacts [decidable.is_false hp, decidable.is_true hp],
end

[Violeta Hernández]

Any idea where this could go?

[Junyan Xu]

The equivalence? Just below docs#set.to_finset ?

[Violeta Hernández]

By the way, I'm thinking about renaming finsupp.equiv_fun_on_fintype to fintype.finsupp_equiv_fun

[Violeta Hernández]

Seems like a much more straightforward name

[Violeta Hernández]

Do we have support for that? (pun intended)

[Yaël Dillies]

I would even be happy with finsupp_equiv_fun