finset from "finsubtype"

Stream: maths

[Paul van Wamelen]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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]

Thank you!!