Bijection between Finset and Fin n

Stream: Is there code for X?

[Swarnava Chakraborty]

Is there any way I can construct an explicit bijection between Finset and Fin n , where n is the cardinality of the Finset? Does it already exist?

[Riccardo Brasca]

What do you mean by "explicit"? Anyway we have Finset.equivFin and friends.

[Riccardo Brasca]

If you want to actually compute with it there is Fintype.truncEquivFin

[Swarnava Chakraborty]

Thanks. I am new to Lean and do not really understand the function type ≃ notation.My question was how to construct a bijection. What equivFin does is I think gives all the possible bijections, right?

[Edward van de Meent]

it does not. it just uses choice to get one

[Edward van de Meent]

the ≃ notation refers to docs#Equiv, which is a datastructure containing maps either way and a proof that these are left and right inverse to eachother. This means that equivFin contains a map s -> Fin s.card and a map Fin s.card -> s which are eachothers inverse. it produces this map by using choice, so there is no telling what 0:Fin s.card concretely maps to in s.

[Edward van de Meent]

truncEquivFin refers to the fact that, because Fintype stores the concrete elements of the type up to permutation, if you choose a permutation, you can also computably get a concrete bijection. This allows for making computable functions which evaluate such a bijection, so long as the return value doesn't change no matter which bijection you pick.