Iterate through every function from fintype to fintype

Stream: general

[Jihoon Hyun]

As in the title, I'd like to iterate through all possible functions f : α → β where Fintype α and Fintype β.
The goal is to return true if there is no f which g : (α → β) → Bool returns false, or false otherwise.
How should I achieve this?

[Yaël Dillies]

Are you looking for docs#Pi.fintype ?

[Jihoon Hyun]

That's not a primary goal, but it seems like I can just use Fintype.elems from there. Still, is there a more direct way?

[Yaël Dillies]

Does that fit the bill?

import Mathlib.Data.Fintype.Pi

def allTrue {α β : Type*} [DecidableEq α] [Fintype α] [Fintype β] (g : (α → β) → Bool) : Bool :=
  ∀ f, g f

[Jihoon Hyun]

Yes, that does the work! Thanks!