finite sets

[PatrickMassot]

We need to explain the finset vs fintype vs finite mess somewhere, probably in Chapter 4.

[avigad]

I'd rather save this for a chapter on discrete mathematics. We should have examples of various kinds of proof by induction, and combinatorial reasoning with finite sets, finite sums, cardinality, etc., etc. I think the subject matter all hangs together, and there is a coherent story there.

So maybe the next few chapters are:

• types, structures, and number systems
• algebra
• topology
• discrete mathematics

[PatrickMassot]

I fear both algebra and topology make use of what you can discrete mathematics.

[avigad]

Two options there:

• Put the discrete math chapter first.
• If the only uses are mild (like a straightforward definition by recursion or induction), just do them on the fly and leave the more elaborate stuff for later.

I still think it makes sense to group induction, finsets, finite sums and products together, and cardinality together, and take the time to do them thoroughly. It feels like a different topic from basic set theory.

[avigad]

The wiki page now mentions the plan to have a discrete math chapter that does finiteness.