Zulip Chat Archive

Stream: Is there code for X?

Topic: fintype (s.to_set)


view this post on Zulip Scott Morrison (Apr 12 2020 at 10:48):

How did I not know this stream existed?!

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:48):

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

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

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:53):

Ta!

view this post on Zulip Kenny Lau (Apr 12 2020 at 10:53):

found by examining the proof of finset.finite_to_set

view this post on Zulip 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: May 07 2021 at 18:19 UTC