Zulip Chat Archive

Stream: Is there code for X?

Topic: fintype (s.to_set)


Scott Morrison (Apr 12 2020 at 10:48):

How did I not know this stream existed?!

Scott Morrison (Apr 12 2020 at 10:48):

instance {α : Type*} (s : finset α) : fintype (s.to_set) := sorry

Kenny Lau (Apr 12 2020 at 10:53):

instance finset.to_set.fintype {α : Type*} (s : finset α) : fintype (s.to_set) :=
fintype.of_finset s $ λ _, iff.rfl

Scott Morrison (Apr 12 2020 at 10:53):

Ta!

Kenny Lau (Apr 12 2020 at 10:53):

found by examining the proof of finset.finite_to_set

Kevin Buzzard (Apr 12 2020 at 10:54):

I didn't know about this stream either -- I found out about an hour ago, and as a result 1000 people just got an email.


Last updated: Dec 20 2023 at 11:08 UTC