## Stream: general

### Topic: finset vs finite

#### Johan Commelin (Sep 28 2018 at 13:31):

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 (Sep 28 2018 at 13:43):

Aaah, finite_mem_finset can help me.

#### Rob Lewis (Jan 31 2019 at 21:27):

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 (Jan 31 2019 at 21:28):

Currently we only have finset.univ.filter

#### Kenny Lau (Jan 31 2019 at 21:28):

finset.univ.filter

#### Rob Lewis (Jan 31 2019 at 21:29):

That'll work, thanks.

Last updated: May 08 2021 at 19:11 UTC