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