## Stream: Is there code for X?

### Topic: fintype.of_finset alternative

#### 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.

#### Hanting Zhang (Apr 05 2021 at 23:21):

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

:face_palm:

#### 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