Zulip Chat Archive

Stream: maths

Topic: fincard and cardinal.to_nat


view this post on Zulip Aaron Anderson (Feb 18 2021 at 04:04):

On branch#cardinal_to_nat, I've added a function cardinal.to_nat and used it to make a function fincard that can give a N-valued cardinality for any type. This is the same construction used in the linear algebra library to define findim.

view this post on Zulip Aaron Anderson (Feb 18 2021 at 04:05):

If people think this is a good idea, I will adapt some more of the API for a similar fincard function used in this project: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/finsum/basic.lean

view this post on Zulip Aaron Anderson (Feb 18 2021 at 04:05):

and then PR it.

view this post on Zulip Aaron Anderson (Feb 18 2021 at 04:07):

I also think it'd be useful to add an enat version, if only to be able to state things in a way that doesn't wig out people who intuitively don't want the cardinality of an infinite set to be 0.

view this post on Zulip Aaron Anderson (Feb 18 2021 at 04:07):

Obviously the first function would be named cardinal.to_enat, but what should the extended version of fincard be called?

view this post on Zulip Johan Commelin (Feb 18 2021 at 04:25):

This sounds like a very good idea. There has been talk about fincard for a long time on zulip, and I'm glad someone is actually picking it up.

view this post on Zulip Aaron Anderson (Feb 18 2021 at 06:04):

If I move fincard to a separate file, should it be under data? set_theory?

view this post on Zulip Johan Commelin (Feb 18 2021 at 06:22):

data/fintype/card.lean currently contains stuff that doesn't have to do anything with card at all :frown: :head_bandage: otherwise that would be a natural place, I guess

view this post on Zulip Johan Commelin (Feb 18 2021 at 06:22):

set_theory (to me) is about ZFC specific stuff

view this post on Zulip Johan Commelin (Feb 18 2021 at 06:22):

data sounds good to me

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 07:54):

A new fincard file would surely be fine, is there ever an argument against adding a new file with a descriptive name?

view this post on Zulip Jason KY. (Feb 18 2021 at 10:39):

Aaron Anderson said:

If people think this is a good idea, I will adapt some more of the API for a similar fincard function used in this project: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/finsum/basic.lean

There is some APIs for this on the fincard branch of mathlib which can be useful I hope. However, it's mostly for finsum so I'm not sure if its helpful after all
https://github.com/leanprover-community/mathlib/blob/fincard/src/data/fincard.lean

view this post on Zulip Aaron Anderson (Mar 01 2021 at 20:09):

#6494


Last updated: May 10 2021 at 08:14 UTC