Bijection between finset and its cardinality

Stream: new members

[Minsung C]

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]

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

[Eric Wieser]

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

[Yakov Pechersky]

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]

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]

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