Sum of finite types

Stream: Is there code for X?

[Egbert Rijke]

Hi!

I have a very quick question. Is there a bijection between Sigma types of standard finite types Fin and the standard finite type with the sum as the number of elements?

I tried to look for it in mathlib, but I couldn't spot it anywhere.

Many thanks!

[Markus Himmel]

@loogle Fin, Sum

[Markus Himmel]

The bot won't answer me, but I think you're looking for docs#finSumFinEquiv

[Notification Bot]

This topic was moved here from #general > Sum of finite types by Mario Carneiro.

[Egbert Rijke]

Thanks! I'm looking for the version of that for Sigma types

[Markus Himmel]

Could you give a Lean statement of the equivalence you're looking for?

[Egbert Rijke]

Hm... the following might not exactly be valid lean syntax, but this is what I am looking for:

theorem foo :
  (n : ℕ) (f : Fin n → ℕ) →
  (Fin (∑ i < n, f i)) ≃ (∑ i ∈ Fin n, Fin (f i)) := sorry

[Yaël Dillies]

We don't have it, but docs#finPiFinEquiv is very close and you should get inspiration from it

[Egbert Rijke]

Thanks!

[Egbert Rijke]

Is there perhaps another way in which you count elements of Sigma types, or is counting just not something that happens in mathlib?

[Floris van Doorn]

docs#Fintype.card_sigma, docs#Cardinal.mk_sigma, docs#Finset.card_sigma, docs#Finset.card_sigmaLift are some versions, depending on what you want.

[Floris van Doorn]

The first one, together with docs#Fintype.equivFinOfCardEq will also produce the other equivalence you looked for (not computably though).

[Eric Wieser]

docs#FinEnum.instSigma might be another answer to your question, if by "count" you mean "enumerate"