## Stream: Is there code for X?

### Topic: fincard X^Y

#### Kevin Buzzard (Sep 03 2020 at 04:50):

instance (X : Type) [fintype X] (Y : Type) [fintype Y] : fintype (X → Y) := sorry


It wouldn't surprise me if we knew |X->Y|=|Y|^|X| for e.g. cardinals, and I'm hoping to be able to extract the corresponding nat-valued fact for fintypes.

#### Kenny Lau (Sep 03 2020 at 04:51):

docs#fintype.card_pi

Last updated: May 17 2021 at 15:13 UTC