set finset etc

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

@Jeremy Avigad I remember that as a newbie I was very confused about

{ x | p x}
-- vs
{ x // p x}

It would be nice if you could integrate some wisdom about the pros and cons of the two into your talk on setty things.

[Yury G. Kudryashov]

The fact that this notation is defined in C++ doesn't help here. I remember myself trying to grep for notation.*{

[Jeremy Avigad]

Will do. I am about to start working on the set theory chapter of MiL. Here is the current plan: https://github.com/avigad/mathematics_in_lean_source/wiki. Other comments and suggestions for that chapter (or in general) are welcome.