finset of functions

Stream: Is there code for X?

[Bolton Bailey]

Given a fintype A and s : finset B, how does one get the finset of all functions from A to B with image in s?

[Kyle Miller]

docs#fintype.pi_finset I believe

import data.fintype.basic

open_locale classical

noncomputable
example (A B : Type*) [fintype A] (s : finset B) : finset (A → B) := fintype.pi_finset (λ a, s)

[Kyle Miller]

Then docs#fintype.mem_pi_finset gives you the membership property

[Yaël Dillies]

You probably rather want docs#finset.pi, except that the return type is a bit offputting. Guess who got confused again