Zulip Chat Archive

Stream: new members

Topic: Bijection between finset and its cardinality


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!

Eric Wieser (Apr 08 2021 at 17:12):

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

Eric Wieser (Apr 08 2021 at 17:14):

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

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.

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!

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: Dec 20 2023 at 11:08 UTC