Zulip Chat Archive
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):
Last updated: May 02 2025 at 03:31 UTC