## Stream: maths

### Topic: coe_sort for finset

#### Enrico Borba (Jan 14 2020 at 04:56):

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 (Jan 14 2020 at 05:21):

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 (Jan 14 2020 at 08:06):

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 (Jan 14 2020 at 08:12):

@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 (Jan 14 2020 at 08:37):

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 (Jan 14 2020 at 08:38):

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 (Jan 14 2020 at 08:39):

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

#### Enrico Borba (Jan 14 2020 at 08:43):

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

#### Enrico Borba (Jan 14 2020 at 08:43):

I think I understand. Thank you

#### Johan Commelin (Jan 14 2020 at 08:46):

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

#### Enrico Borba (Jan 14 2020 at 08:50):

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 (Jan 14 2020 at 08:55):

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 (Jan 14 2020 at 08:56):

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

#### Kevin Buzzard (Jan 14 2020 at 08:58):

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 (Jan 14 2020 at 09:11):

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

#### Enrico Borba (Jan 15 2020 at 04:35):

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 (Jan 15 2020 at 04:38):

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 (Jan 15 2020 at 05:33):

That's awesome! Thanks a ton.

Last updated: May 18 2021 at 08:14 UTC