Zulip Chat Archive

Stream: Is there code for X?

Topic: fintype.of_finset alternative


view this post on Zulip Adam Topaz (Apr 05 2021 at 23:12):

Do we have a lemma providing a fintype instance on a type X given a finset T : finset X such that every element of X is a member of T? Note that docs#fintype.of_finset doesn't apply directly.

view this post on Zulip Hanting Zhang (Apr 05 2021 at 23:21):

I think that is exactly the definition of docs#fintype. Maybe \<T, hT\> would work directly.

view this post on Zulip Adam Topaz (Apr 05 2021 at 23:24):

:face_palm:

view this post on Zulip Adam Topaz (Apr 05 2021 at 23:24):

I don't understand finite things in lean


Last updated: May 17 2021 at 14:12 UTC