Finset of all functions from a fin type with image in finset

Stream: Is there code for X?

[Bolton Bailey]

Is there a function with the type signature def foo {A B : Type} [fintype A] (S : finset B) : finset (A -> B) := sorry which returns the set of all functions with images subset of B?

[Eric Wieser]

By which you mean, ∀ f ∈ foo S, finset.univ.image f ⊆ S?

[Eric Wieser]

(finset.univ : finset (A → S)).map ⟨(∘ coe), sorry⟩ should do the trick

[Yakov Pechersky]

docs#function.embedding.subtype for the map if that helps with the composition proof

[Bolton Bailey]

import data.mv_polynomial.basic

def foo (A B : Type) [fintype A] (S : finset B) : finset (A -> B) :=
  (finset.univ : finset (A → S)).map ⟨(∘ coe), sorry⟩

What do I have to import to synthesize fintype (A → ↥S)?

[Alex J. Best]

open_locale classical or add some decidability assumptions, look at docs#pi.fintype.

import data.mv_polynomial.basic
open_locale classical
noncomputable
def foo (A B : Type) [fintype A] (S : finset B) : finset (A -> B) :=
  (finset.univ : finset (A → S)).map ⟨λ f z, f z, sorry⟩

[Bolton Bailey]

For future reference, I found this way of writing it

def function_finset (A : Type) (B : Type) [DecidableEq A] [Fintype A] (S : Finset B) : Finset (A -> B) :=
  Fintype.piFinset (fun _ => S)

[Yaël Dillies]

Yes, this is the canonical spelling.

[Bolton Bailey]

Is there interest in putting in a definition for this, or should I s/function_finset/Fintype.piFinset (fun _ => S)/g my file?

[Eric Wieser]

I think probably the latter

[Eric Wieser]

You could use Fintype.piFInset (Function.const S) if you prefer

[Yaël Dillies]

In LeanAPAP, we defined notation for it, but I really see no point in having a separate definition.