## Stream: maths

### Topic: finset from "finsubtype"

#### Paul van Wamelen (Jan 09 2021 at 21:58):

Is the following true?

import data.fintype.basic

example {α : Type*} {p : α → Prop} (h : fintype {x // p x}) :
∃ (s : finset α), ↑s = { x | p x }


#### Kevin Buzzard (Jan 09 2021 at 22:06):

Yes. The stuff you're missing is in data.set.finite.

#### Kevin Buzzard (Jan 09 2021 at 22:07):

It's all noncomputable so it's somehow separated off.

#### Mario Carneiro (Jan 09 2021 at 22:07):

import data.fintype.basic
import data.set.finite

example {α : Type*} {p : α → Prop} (h : fintype {x // p x}) :
∃ (s : finset α), ↑s = { x | p x } :=
set.finite.exists_finset_coe ⟨h⟩


#### Kevin Buzzard (Jan 09 2021 at 22:11):

PS it's come to something when a mathematician has to check to see if a finite set is finite :-) I guess this is what Lean does to us. Type theory has some weird surprises :-/

#### Mario Carneiro (Jan 09 2021 at 22:11):

You can also do it without referencing finite:

import data.fintype.basic

example {α : Type*} {p : α → Prop} (h : fintype {x // p x}) :
∃ (s : finset α), ↑s = { x | p x } :=
⟨@set.to_finset _ _ h, @set.coe_to_finset _ _ h⟩


#### Paul van Wamelen (Jan 10 2021 at 03:02):

Thank you!!

Last updated: May 09 2021 at 10:11 UTC