Bounded Fintype

Stream: mathlib4

[Gareth Ma]

Hi, I am trying to express the set of k-tuples on a n-element ordered alphabet. I want to count stuff like "how many tuples are strictly increasing?". Can someone provide guidance on how concretely?
I got advice to represent it as functions from Fin k \to \iota, where \iota is a Fintype with a linear order, but I am not sure how to correspond the n-element ordered alphabet with a Fintype.

[Kevin Buzzard]

So is the question "I have a linearly ordered Fintype, can someone produce an order isomorphism with fin n for some n"? If not, can you post code which asks your actual question rather than asking it in words? Asking to fill in a sorry in a #mwe is the best way to ask questions here.

[Yaël Dillies]

Yeah, it sounds like you could just use Fin k → Fin n here.

[Gareth Ma]

A0AC44F5-4AEE-4215-8D53-D6A26397256A.png

[Gareth Ma]

Here it is: the number of 3-tuple of alphabets such that the final one is Z and they’re strictly increasing

[Gareth Ma]

Yaël Dillies said:

Yeah, it sounds like you could just use Fin k → Fin n here.

I assume I add a LinearOrder to the fin n too?

[Eric Wieser]

No, Fin n already has one

[Gareth Ma]

I see, okay thanks!

[Gareth Ma]

I think this is what Bhavik recommended me too (the original suggestion) but I misunderstood it