coe_sort for finset

Stream: maths

[Enrico Borba]

I'm trying to prove (in Lean) the statement that the cardinality of $\text{End}(A)$ where $A$ is a finite set is equal to $|A|^{|A|}$. However, I'm having a hard time just stating it in Lean. What I tried was

theorem finset_endomorphism_cardinality {α : Type*} (s : finset α) :
    finset.card (↥s → ↥s) = (finset.card s) ^ (finset.card s) :=
  sorry

However, it doesn't seem that coe_sort exists for finset. I'm wondering: 1) what is a working way to state this now, 2) Is there a need for coe_sort in finset?

[Bryan Gin-ge Chen]

I think this is may be what you want:

import data.finset

theorem finset_endomorphism_cardinality {α : Type*} [decidable_eq α] (s : finset α) :
    finset.card (s.pi (λ _, s) ) = (finset.card s) ^ (finset.card s) :=
begin
  simp only [finset.card, finset.pi, multiset.card_pi,
    multiset.prod_repeat, multiset.map_const, nat.pow_eq_pow]
end

[Kevin Buzzard]

Finite sets are a great example of where Lean proofs can look very different to what I write on the board. The book I used in my intro to proof course had a "multiplication principle" which said that if you had an $n$-step process and you could do the $$i$$th step in $a_i$ ways (independent of what happened in the other steps) then clearly the number of ways you could complete the process was $\prod_{i=1}^na_i$. No proof was offered and the result was taken as fundamental and used to compute things like the number of maps from a finite set $A$ to a finite set $B$ (building the function element by element). Had this stuff not been possible in Lean it would have been hard to stick with it, but there was this gigantic multiset and finset library in place which proved everything rigorously, and I learnt that looking through these files and just reading the statements of the lemmas could teach me a lot. Each one was trivial (most followed from the multiplication principle or even simple principles ;-) ) but it was good to see that they were there.

[Johan Commelin]

@Enrico Borba Do you want finset or fintype? The difference can at first be confusing for mathematicians. But think of set as "subset" and type as "set".

[Enrico Borba]

I guess I want fintype since I’m looking to talk about functions with these finite sets as domains and images. What’s the distinction between finset and fintype?

[Johan Commelin]

A fintype is a type with only finitely many terms (i.e. elements).
A finset is a finite subset of an arbitrary type.

[Johan Commelin]

You can naturally talk about functions between types. But not (naturally) about functions between subsets.

[Enrico Borba]

This cleared some things up for me: https://github.com/leanprover-community/mathlib/blob/master/docs/theories/sets.md

[Enrico Borba]

I think I understand. Thank you

[Johan Commelin]

If you use fintype, you'll probably have an easier time proving your theorem

[Enrico Borba]

Likely yes. I’m also trying to understand Lean’s type system while I learn these things. I didn’t realize it would implicitly coerce sets to types, which is why finsets caught me off guard a bit.

[Kevin Buzzard]

Sets were a point of confusion for me for quite a while! A term of type set X is really a term, not a type, so you are limited in what you can do with it (e.g. you can't define a function from A : set X to a type, even though mathematicians would have no trouble doing this).

[Kevin Buzzard]

The corresponding subtype contains precisely the same information, just packaged in a different way.

[Kevin Buzzard]

That page in the docs you link to was written by Patrick and Chris. When I was learning, I didn't know enough about Lean to be able to write docs; now I understand a lot more stuff and tend not to write docs because I understand it and I don't know what docs people need! Do you have any doc requests?

[Patrick Massot]

I don't think I wrote any of that page, I think it's all from Chris.

[Enrico Borba]

I think this is may be what you want:

import data.finset

theorem finset_endomorphism_cardinality {α : Type*} [decidable_eq α] (s : finset α) :
    finset.card (s.pi (λ _, s) ) = (finset.card s) ^ (finset.card s) :=
begin
  simp only [finset.card, finset.pi, multiset.card_pi,
    multiset.prod_repeat, multiset.map_const, nat.pow_eq_pow]
end

@Bryan Gin-ge Chen How did you know which definitions to pass to simp? by simp * works, but I'd like a way to know which simplifications it applied so I can rewrite it as a simp only.

[Bryan Gin-ge Chen]

You can use squeeze_simp to give you a minimal set. It usually works, but it's not perfect. Sometimes there are extra / missing lemmas.

[Enrico Borba]

That's awesome! Thanks a ton.