Image of function as finset

Stream: Is there code for X?

[Adam Topaz]

Given a type X with [fintype X] and a function f : X \to Y, what's the best way to construct the image of f as a finset Y?

[Eric Wieser]

I guess docs#finset.image doesn't help?

[Eric Wieser]

(finset.univ : finset X).image f looks like it should work

[Eric Wieser]

I don't think there's a finset.range to match set.range

[Adam Topaz]

Yeah the finest.univ trick should do the trick

[Bhavik Mehta]

Adam Topaz said:

Yeah the finest.univ trick should do the trick

Yup this is what I usually use to express this

[Eric Wieser]

It's probably quite reasonable to introduce a finset.range though, since definitionally that might avoids \mem univ here and there

[Eric Wieser]

It would match docs#set.range and docs#monoid_hom.range etc

[Eric Rodriguez]

if it's an embedding, docs#finset.map is really solid too; has good cardinality results and such liek