s equiv s.to_finset

Stream: Is there code for X?

[Eric Rodriguez]

do we really not have:

example {a} {s : set a} [fintype s] : s.to_finset ≃ s

[Yaël Dillies]

The correct thing to ask for is

def finset.coe_equiv {α : Type*} (s : finset α) : (s : set α) ≃ s := equiv.refl _

[Eric Rodriguez]

but I want to make an equiv from docs#simple_graph.edge_finset to its edge_set

[Yaël Dillies]

Then you can compose that with docs#equiv.subtype_equiv_prop (whose name is very hard to guess :thinking:)

example {a} {s : set a} [fintype s] : s.to_finset ≃ s :=
(finset.coe_equiv _).symm.trans $ equiv.subtype_equiv_prop s.coe_to_finset

[Yaël Dillies]

Because finset.coe_equiv is refl, I guess you can use equiv.subtype_equiv_prop s.coe_to_finset directly.