fintype arrow

Stream: Is there code for X?

[Joachim Breitner]

I find lemmas like

prod.fintype : Π (α : Type u_1) (β : Type u_2) [_inst_1 : fintype α] [_inst_2 : fintype β], fintype (α × β)

but oddly not

? : Π (α : Type u_1) (β : Type u_2) [_inst_1 : fintype α] [_inst_2 : fintype β], fintype (α → β)

Did I just not search well enough? Or does this not hold because function equality is not extensional?

[Eric Rodriguez]

pi.fintype should exist; and A \to B is defeq to \pi A, B

[Joachim Breitner]

Ah, indeed, but it requires decidable equality: https://leanprover-community.github.io/mathlib_docs/data/fintype/basic.html#pi.fintype.

Guess I’ll add that condition to my theorems for now and worry later about whether that’s a problem or not.

[Gabriel Ebner]

Ah, indeed, but it requires decidable equality:

This is mildly surprising, does anybody know why?

[Yaël Dillies]

It all comes from docs#multiset.pi.cons

[Yaël Dillies]

I never really understood the return type of docs#finset.pi either. The design of this bit of the library is quite obscure to me...

[Joachim Breitner]

Oddly, I don’t have this constraint on https://leanprover-community.github.io/mathlib_docs/data/fintype/basic.html#fintype.card_set (which is about α → Prop)

[Yaël Dillies]

Yeah because this is classical already

[Reid Barton]

Gabriel Ebner said:

Ah, indeed, but it requires decidable equality:

This is mildly surprising, does anybody know why?

fintype without decidable equality is a weird thing to begin with.
I don't see how to go about enumerating the functions from α to bool without having decidable equality on α.

[Gabriel Ebner]

Ah, that's what I was missing. The enumerating part is easy and doesn't require decidable equality, but then you need to make an if-then-else to get a function.