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