finset vs finite

Stream: general

[Johan Commelin]

What are the pros and cons of finset vs finite? I'm quite confused how to move back and forth between the two. Related: Should there be a lemma that every set of a fintype is finite? Maybe it is even there, but I couldn't find it.

[Johan Commelin]

Aaah, finite_mem_finset can help me.

[Rob Lewis]

I just found this looking for an answer to my question, which is basically the same as Johan's from September: is there a canonical way to carve a finset out of a fintype? Something like def sep {α} [fintype α] (P : α → Prop) : finset α?

[Johannes Hölzl]

Currently we only have finset.univ.filter

[Kenny Lau]

finset.univ.filter

[Rob Lewis]

That'll work, thanks.