Finite sets/types docs

Stream: general

[Johan Commelin]

Mental note: we should update https://leanprover-community.github.io/theories/sets.html now that the finite typeclass exists.

[Chris Hughes]

I think I wrote that a very long time ago. I didn't understand Lean that well at the time, so I think it might not be the most helpful anyway.

[Wrenna Robson]

It is slightly counterintuitive that the definition of set.finite s is not finite s.

[Kyle Miller]

@Wrenna Robson It's that way because finite is newer. I believe @Yury G. Kudryashov has a PR somewhere that updates set.finite.

[Wrenna Robson]

Right, when I spoke to Yaël about it earlier today they made it sound like it would be staying as it is.

[Yaël Dillies]

I thought we wouldn't switch to that definition because that would make set.finite a class, hence frozen in the local context.