Zulip Chat Archive

Stream: maths

Topic: finset from "finsubtype"


view this post on Zulip 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 }

view this post on Zulip Kevin Buzzard (Jan 09 2021 at 22:06):

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

view this post on Zulip Kevin Buzzard (Jan 09 2021 at 22:07):

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

view this post on Zulip 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

view this post on Zulip 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 :-/

view this post on Zulip 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

view this post on Zulip Paul van Wamelen (Jan 10 2021 at 03:02):

Thank you!!


Last updated: May 09 2021 at 10:11 UTC