Zulip Chat Archive

Stream: new members

Topic: Bijection between finset and its cardinality


view this post on Zulip Minsung C (Apr 08 2021 at 17:08):

Hi everyone,

I'm trying to find a lemma that says there exists a bijection between a finset and its cardinality. I saw in the library that there exists what I want for fintypes: fintype.equiv_fin T where T is a fintype. But finset.equiv_fin doesn't exist.
Is there something like this for finsets, or is my best bet to use fintype.of_finset to convert it into a fintype and work from there?
I want finsets in particular because I'm working with finite subsets of N\mathbb{N} and I want to take the min/Inf of said sets (which, unluckily, seem to only take in finsets).

Thanks!

view this post on Zulip Eric Wieser (Apr 08 2021 at 17:12):

Can you prove a #mwe showing what type you want out?

view this post on Zulip Eric Wieser (Apr 08 2021 at 17:14):

docs#set.finite.fin_embedding is probably close to what you want

view this post on Zulip Yakov Pechersky (Apr 08 2021 at 17:43):

bijection between a finset and its cardinality

An equiv is between types, so you'd have to coerce the finset to a Sort (and the cardinality to a Sort, which would be fin n) to have an equiv. Which is exactly what your thought of fintype.of_finset combined with fintype.equiv_fin would give you.

view this post on Zulip Minsung C (Apr 08 2021 at 17:51):

Yakov Pechersky said:

bijection between a finset and its cardinality

An equiv is between types, so you'd have to coerce the finset to a Sort (and the cardinality to a Sort, which would be fin n) to have an equiv. Which is exactly what your thought of fintype.of_finset combined with fintype.equiv_fin would give you.

This was exactly the issue I had while trying to make an mwe for Eric. Still getting used to the whole sets vs types thing. Will try this out...thank you!

view this post on Zulip Eric Wieser (Apr 08 2021 at 17:53):

fintype.equiv_fin (s : set _) may be what you're after, for some finset s


Last updated: May 12 2021 at 05:19 UTC