fincard and cardinal.to_nat

Stream: maths

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Aaron Anderson]

and then PR it.

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Johan Commelin]

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.

[Aaron Anderson]

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

[Johan Commelin]

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

[Johan Commelin]

set_theory (to me) is about ZFC specific stuff

[Johan Commelin]

data sounds good to me

[Kevin Buzzard]

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

[Jason KY.]

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

[Aaron Anderson]

#6494