relabeling Fin n

Stream: Is there code for X?

[Alex Kontorovich]

Suppose I have a map f : Fin n → X, and a subset S of Fin n of cardinality m = S.card; I'd like to create a map g : Fin m → Xby restricting f to the elements of S. Is there a clean way to do this? Thanks!

[Adam Topaz]

docs#fintype.equiv_fin composed with f, I suppose?

[Adam Topaz]

you may need to cast to get the right m in the fin m as well, but that should be straightforward.

[Eric Wieser]

Can you write out the full mwe?

[Eric Wieser]

This sounds like something that can be done computably if the details are what I think they are

[Eric Wieser]

(concretely, I think the statement I think we should have is [FinEnum X] (s : Finset X) : FinEnum s)

[Alex Kontorovich]

That's great, thanks! I'll try to play with that in my application...