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