Resources for finite sets/types

Stream: Lean for teaching

[Miguel Marco]

Hi all,

I am giving an informal course of interactive proving with lean, for mathematics undergrad students.

I considered talking about finite sets and types, but haven't been able to think of a nice way to present them (mostly because the multiple incarnations of similar concepts: fintype, finset, finite and set.finite).

Do you know if there is some teaching material that covers that ?

[Kevin Buzzard]

yeah I tend to avoid finiteness. Did you talk about sets? If you have already explained sets then finset is I guess the obvious next thing.

[Patrick Massot]

I certainly avoid finiteness in my teaching, but the goal is to teach math, not Lean.

[Jeremy Avigad]

Miguel, I am currently teaching a similar undergraduate class, and I have a bit of material that I used in lectures to give students some pointers about finite sets and structures. It's not really suitable for public consumption but I am planning to work it into another Mathematics in Lean chapter in the spring. In the meanwhile, I can share some of the material with you offline, if you would like.

[Miguel Marco]

Jeremy Avigad said:

Miguel, I am currently teaching a similar undergraduate class, and I have a bit of material that I used in lectures to give students some pointers about finite sets and structures. It's not really suitable for public consumption but I am planning to work it into another Mathematics in Lean chapter in the spring. In the meanwhile, I can share some of the material with you offline, if you would like.

That would be very helpful. Can you please email it to me?

[Sina]

@Jeremy Avigad I'd be interested too, since I have a student who is doing a final project on adjacency matrices of finite simple graphs, and so far my advice to him was to just do it for arbitrary types and avoid finiteness (as Kevin also said), but it would be nice to have some concrete finite types to reduce/eval some basic computation with adj matrices.