Zulip Chat Archive

Stream: new members

Topic: Understanding Set and finset better


view this post on Zulip ROCKY KAMEN-RUBIO (Jun 18 2020 at 20:34):

Has anyone written any tutorials on sets and finsets/fintypes/nodeup/card? I'm having trouble understanding what's going on just from the documentation.

view this post on Zulip Patrick Massot (Jun 18 2020 at 20:39):

we have https://leanprover-community.github.io/theories/sets.html

view this post on Zulip Bhavik Mehta (Jun 18 2020 at 20:54):

If your goal is to use finsets, fintype and card, I'd suggest looking at the theorem statements in data.finset and data.fintype, and totally ignoring nodup

view this post on Zulip Bhavik Mehta (Jun 18 2020 at 20:55):

There's a very thorough finset API (albeit not the best documented) but at no point should you need to worry about how a finset is actually implemented

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 19 2020 at 00:28):

Bhavik Mehta said:

There's a very thorough finset API (albeit not the best documented) but at no point should you need to worry about how a finset is actually implemented

That's good to know. A lot of my confusion was coming from the implementation so I'll try ignoring that and see if I can make better sense of it.


Last updated: May 10 2021 at 18:22 UTC